File tree Expand file tree Collapse file tree
Mathlib/Analysis/InnerProductSpace Expand file tree Collapse file tree Original file line number Diff line number Diff line change @@ -394,7 +394,7 @@ theorem normDet_eq_abs_det (f : U →ₗ[ℝ] U) : f.normDet = |f.det| := by
394394 simpa using f.normDet_eq_norm_det
395395
396396/--
397- Using Hausdorff measure wih the domain dimension, the volume of the image is scaled by
397+ Using Hausdorff measure with the domain dimension, the volume of the image is scaled by
398398`LinearMap.normDet`.
399399-/
400400theorem hausdorffMeasure_image [MeasurableSpace U] [BorelSpace U] [MeasurableSpace V] [BorelSpace V]
@@ -420,7 +420,7 @@ theorem hausdorffMeasure_image [MeasurableSpace U] [BorelSpace U] [MeasurableSpa
420420 simp [Real.hausdorffMeasure_of_finrank_lt h]
421421
422422/--
423- Using Euclidean Hausdorff measure wih the domain dimension, the volume of the image is scaled by
423+ Using Euclidean Hausdorff measure with the domain dimension, the volume of the image is scaled by
424424`LinearMap.normDet`.
425425-/
426426theorem euclideanHausdorffMeasure_image [MeasurableSpace U] [BorelSpace U] [MeasurableSpace V]
You can’t perform that action at this time.
0 commit comments