Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-11-09 17:46
b9c3765b
View on Github →
feat: Prove that a fundamental domain has nonzero volume (
#8287
)
Estimated changes
Modified
Mathlib/Algebra/Module/Zlattice.lean
added
theorem
Zspan.measure_fundamentalDomain_ne_zero
Modified
Mathlib/MeasureTheory/Group/FundamentalDomain.lean
added
theorem
MeasureTheory.IsFundamentalDomain.measure_ne_zero