Predicates on Modules

Modules and potential elements can be tested against each other for a few properties.

M eq N : ModDed, ModDed -> BoolElt
Return true if M and N are equal as modules.
x in M : Any, ModDed -> BoolElt
Return true if x can be coerced into the module M.
M subset N : ModDed, ModDed -> BoolElt
Return true if M is a submodule of N. An embedding map of M in N can be returned by IsSubmodule(M, N).
V2.28, 13 July 2023