Commit 2023-09-21 17:41 95aba723

View on Github →

feat: the Unfolding Trick (#6223) This PR is a forward port of mathlib3 PR !3#18863

Estimated changes

Modified Mathlib/GroupTheory/GroupAction/Group.lean

added def DistribMulAction.toAddEquiv₀

Modified Mathlib/MeasureTheory/Group/FundamentalDomain.lean

added theorem MeasureTheory.IsFundamentalDomain.integral_eq_tsum''

added theorem MeasureTheory.IsFundamentalDomain.lintegral_eq_tsum''

Modified Mathlib/MeasureTheory/Measure/Haar/Quotient.lean

modified theorem MeasurePreservingQuotientGroup.mk'

added theorem MeasureTheory.IsFundamentalDomain.absolutelyContinuous_map

modified theorem MeasureTheory.IsFundamentalDomain.map_restrict_quotient

added theorem QuotientAddGroup.integral_mul_eq_integral_automorphize_mul

added theorem QuotientGroup.integral_eq_integral_automorphize

added theorem QuotientGroup.integral_mul_eq_integral_automorphize_mul

added theorem essSup_comp_quotientGroup_mk

Modified Mathlib/Topology/Algebra/InfiniteSum/Basic.lean

added theorem AddAction.automorphize_smul_left

added theorem MulAction.automorphize_smul_left

added theorem QuotientAddGroup.automorphize_smul_left

added theorem QuotientGroup.automorphize_smul_left

added theorem tsum_const_smul''

added theorem tsum_const_smul'