feat: port MeasureTheory.Group.Measure (#4496)

leanprover-community · May 30, 2023 · e2aa801 · e2aa801
1 parent 9300e8a
commit e2aa801
Show file tree

Hide file tree

Showing 2 changed files with 849 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1867,6 +1867,7 @@ import Mathlib.MeasureTheory.Function.StronglyMeasurable.Inner
 import Mathlib.MeasureTheory.Group.Action
 import Mathlib.MeasureTheory.Group.Arithmetic
 import Mathlib.MeasureTheory.Group.MeasurableEquiv
+import Mathlib.MeasureTheory.Group.Measure
 import Mathlib.MeasureTheory.Group.Pointwise
 import Mathlib.MeasureTheory.Integral.Lebesgue
 import Mathlib.MeasureTheory.Integral.LebesgueNormedSpace