Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-06-07 04:25
27596b0c
View on Github →
feat: port MeasureTheory.Measure.Haar.Quotient (
#4770
)
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/MeasureTheory/Measure/Haar/Quotient.lean
added
theorem
MeasurePreservingQuotientGroup.mk'
added
theorem
MeasureTheory.IsFundamentalDomain.isMulLeftInvariant_map
added
theorem
MeasureTheory.IsFundamentalDomain.map_restrict_quotient
added
theorem
MeasureTheory.IsFundamentalDomain.smulInvariantMeasure_map