Commit 2024-02-08 16:52 1f7bdd4a

View on Github →

feat(MeasureTheory): integral_comp for LinearIsometryEquiv (#10105) Composition with a LinearIsometryEquiv on a finite dimensional real Hilbert space preserves integrals.

Estimated changes

Modified Mathlib/MeasureTheory/Measure/Haar/InnerProductSpace.lean

added theorem LinearIsometryEquiv.coe_toMeasureEquiv

added theorem LinearIsometryEquiv.measurePreserving

added def LinearIsometryEquiv.toMeasureEquiv

added theorem LinearIsometryEquiv.toMeasureEquiv_symm

Modified Mathlib/MeasureTheory/Measure/Haar/NormedSpace.lean

added theorem MeasureTheory.integrable_comp

added theorem MeasureTheory.integral_comp