Theorem EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp

Modification history

2025-11-04 18:11
Mathlib/MeasureTheory/Measure/Haar/InnerProductSpace.lean
chore: remove redundant measurable space structure on `WithLp` (#31190) …
Added EuclideanSpace.volume_preserving_symm_measurableEquiv_toLpView on Github →