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).

IsFree(M): ModDed -> BoolElt

Return true if \(M\) is a free module.