This file defines the lattice structure on submodules,
⊓ defined as intersection of the underlying carrier.
q are submodules of a module,
p ≤ q means that
p ⊆ q.
Many results about operations on this lattice structure are defined in
most notably those which use
Implementation notes #
This structure should match the
AddSubmonoid.CompleteLattice structure, and we should try
to unify the APIs where possible.
Submodule.mem_iSup is provided in