Skip to content

Commit bd0681b

Browse files
int-y1mo271
andcommitted
feat: port MeasureTheory.Measure.Hausdorff (#4886)
Co-authored-by: Moritz Firsching <firsching@google.com>
1 parent f0892df commit bd0681b

File tree

2 files changed

+1185
-0
lines changed

2 files changed

+1185
-0
lines changed

Mathlib.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2143,6 +2143,7 @@ import Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
21432143
import Mathlib.MeasureTheory.Measure.Haar.NormedSpace
21442144
import Mathlib.MeasureTheory.Measure.Haar.OfBasis
21452145
import Mathlib.MeasureTheory.Measure.Haar.Quotient
2146+
import Mathlib.MeasureTheory.Measure.Hausdorff
21462147
import Mathlib.MeasureTheory.Measure.Lebesgue.Basic
21472148
import Mathlib.MeasureTheory.Measure.Lebesgue.Complex
21482149
import Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

0 commit comments

Comments
 (0)