Theorem ZLattice.comap_toAddSubgroup

Modification history

2025-08-11 22:54
Mathlib/Algebra/Module/ZLattice/Basic.lean
feat(ZLattice/Covolume): add `covolume_div_covolume_eq_relindex` (#25730) …
Added ZLattice.comap_toAddSubgroupView on Github →