Theorem ZLattice.covolume_div_covolume_eq_relindex

Modification history

2025-09-13 17:16
Mathlib/Algebra/Module/ZLattice/Covolume.lean
chore(GroupTheory/Index): rename `relindex` to `relIndex` (#19872) …
Deleted ZLattice.covolume_div_covolume_eq_relindexView on Github →
2025-08-11 22:54
Mathlib/Algebra/Module/ZLattice/Covolume.lean
feat(ZLattice/Covolume): add `covolume_div_covolume_eq_relindex` (#25730) …
Added ZLattice.covolume_div_covolume_eq_relindexView on Github →