Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-28 16:49 958f6b02

View on Github →

refactor(measure_theory/group/fundamental_domain): allow null_measurable_sets (#12005)

Estimated changes

Modified src/measure_theory/group/fundamental_domain.lean

added theorem measure_theory.is_fundamental_domain.image_of_equiv

added theorem measure_theory.is_fundamental_domain.lintegral_eq_tsum

deleted theorem measure_theory.is_fundamental_domain.measurable_set_smul

modified theorem measure_theory.is_fundamental_domain.mk'

modified theorem measure_theory.is_fundamental_domain.null_measurable_set_smul

modified theorem measure_theory.is_fundamental_domain.pairwise_ae_disjoint_of_ac

added theorem measure_theory.is_fundamental_domain.preimage_of_equiv

added theorem measure_theory.is_fundamental_domain.restrict_restrict

added theorem measure_theory.is_fundamental_domain.smul

added theorem measure_theory.is_fundamental_domain.smul_of_comm

added theorem measure_theory.is_fundamental_domain.sum_restrict

Modified src/measure_theory/integral/periodic.lean

Modified src/measure_theory/measure/haar_quotient.lean

deleted theorem measure_theory.is_fundamental_domain.smul