Commit 2025-03-23 14:15 df882075

View on Github →

chore: rename measureEquiv to measurableEquiv (#23230)

Estimated changes

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

added theorem LinearIsometryEquiv.coe_toMeasurableEquiv

deleted theorem LinearIsometryEquiv.coe_toMeasureEquiv

added def LinearIsometryEquiv.toMeasurableEquiv

added theorem LinearIsometryEquiv.toMeasurableEquiv_symm

deleted def LinearIsometryEquiv.toMeasureEquiv

deleted theorem LinearIsometryEquiv.toMeasureEquiv_symm

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