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.
feat(MeasureTheory): integral_comp for LinearIsometryEquiv (#10105) Composition with a LinearIsometryEquiv on a finite dimensional real Hilbert space preserves integrals.