Theorem MeasureTheory.Measure.euclideanHausdorffMeasure_smul₀

Modification history

2026-03-10 05:41
Mathlib/Geometry/Euclidean/Volume/Measure.lean
feat(Geometry/Euclidean): the Euclidean volume measure (#34697) …
Added MeasureTheory.Measure.euclideanHausdorffMeasure_smul₀View on Github →