Theorem ZSpan.isZLattice

Modification history

2025-03-04 13:59
Mathlib/Algebra/Module/ZLattice/Basic.lean
chore(ZLattice): make `ZSpan.isZLattice` an instance (#22530)
Deleted ZSpan.isZLatticeView on Github →
2024-09-09 07:09
Mathlib/Algebra/Module/ZLattice/Basic.lean
chore: rename `Zlattice` -> `ZLattice` (#16622) …
Added ZSpan.isZLatticeView on Github →