Mathlib Changelog
v4
Changelog
About
Github
Theorem
EuclideanSpace.coe_measurableEquiv_symm
Modification history
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_symm
View on Github →