Theorem ZLattice.volume_image_eq_volume_div_covolume

Modification history

2025-08-11 22:54
Mathlib/Algebra/Module/ZLattice/Covolume.lean
feat(ZLattice/Covolume): add `covolume_div_covolume_eq_relindex` (#25730) …
Modified ZLattice.volume_image_eq_volume_div_covolumeView on Github →
2025-04-27 13:12
Mathlib/Algebra/Module/ZLattice/Covolume.lean
chore(*): fix some `Decidable*`/`Fintype` assumptions (#24400) …
Modified ZLattice.volume_image_eq_volume_div_covolumeView on Github →
2024-12-18 15:53
Mathlib/Algebra/Module/ZLattice/Covolume.lean
feat (Lattice/Covolume): Add results linking point counting in lattices and covolume (#12488)
Added ZLattice.volume_image_eq_volume_div_covolumeView on Github →