feat: port MeasureTheory.Measure.FiniteMeasure (#4747)

leanprover-community · Jun 7, 2023 · b1e3dbe · b1e3dbe
1 parent e78e34f
commit b1e3dbe
Show file tree

Hide file tree

Showing 2 changed files with 777 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -2029,6 +2029,7 @@ import Mathlib.MeasureTheory.Measure.AEMeasurable
 import Mathlib.MeasureTheory.Measure.Complex
 import Mathlib.MeasureTheory.Measure.Content
 import Mathlib.MeasureTheory.Measure.Doubling
+import Mathlib.MeasureTheory.Measure.FiniteMeasure
 import Mathlib.MeasureTheory.Measure.GiryMonad
 import Mathlib.MeasureTheory.Measure.Haar.Basic
 import Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace