Commit 2024-03-18 12:19 6aee244f

View on Github →

chore: Define the class IsZlattice (#11356) See the Zulip thread

Estimated changes

modified theorem Zlattice.FG
modified theorem Zlattice.module_finite
modified theorem Zlattice.module_free
modified theorem Zlattice.rank
added theorem Zspan.isZlattice
added theorem Zspan.span_top