Theorem EuclideanSpace.coe_measurableEquiv_symm

Modification history

2026-05-17 20:27
Mathlib/MeasureTheory/Measure/Haar/InnerProductSpace.lean
chore: remove declarations deprecated between 2021-05-15 and 2025-11-15 (#39405) …
Deleted EuclideanSpace.coe_measurableEquiv_symmView on Github →
2025-11-04 18:11
Mathlib/MeasureTheory/Measure/Haar/InnerProductSpace.lean
chore: remove redundant measurable space structure on `WithLp` (#31190) …
Modified EuclideanSpace.coe_measurableEquiv_symmView on Github →
2023-09-13 11:20
Mathlib/MeasureTheory/Measure/Haar/OfBasis.lean
feat: Prove that the measure equivalence between EuclideanSpace ℝ ι and ι → ℝ is volume preserving (#7037) …
Added EuclideanSpace.coe_measurableEquiv_symmView on Github →