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