Theorem Zspan.measure_fundamentalDomain

Modification history

2024-09-09 07:09
Mathlib/Algebra/Module/ZLattice/Basic.lean
chore: rename `Zlattice` -> `ZLattice` (#16622) …
Deleted Zspan.measure_fundamentalDomainView on Github →
2023-09-14 13:42
Mathlib/Algebra/Module/Zlattice.lean
feat: add results for the computation of the volume of Zspan.fundamentalDomain (#6904) …
Added Zspan.measure_fundamentalDomainView on Github →