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