Theorem PiLp.volume_preserving_equiv

Modification history

2025-07-31 10:55
Mathlib/MeasureTheory/Measure/Haar/InnerProductSpace.lean
chore: remove old 2024-04 deprecations (#27713) …
Deleted PiLp.volume_preserving_equivView on Github →
2023-09-13 11:20
Mathlib/MeasureTheory/Measure/Haar/InnerProductSpace.lean
feat: Prove that the measure equivalence between EuclideanSpace ℝ ι and ι → ℝ is volume preserving (#7037) …
Added PiLp.volume_preserving_equivView on Github →