Commit 2026-01-26 19:28 fd5e5373

View on Github →

feat: use measurability as auto-param in MeasurableEquiv (#34457) ... and remove as many explicit proofs as possible.

Estimated changes

Modified Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean

Modified Mathlib/MeasureTheory/Constructions/UnitInterval.lean

Modified Mathlib/MeasureTheory/Group/MeasurableEquiv.lean

Modified Mathlib/MeasureTheory/Group/Prod.lean

Modified Mathlib/MeasureTheory/MeasurableSpace/Embedding.lean

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

modified def LinearIsometryEquiv.toMeasurableEquiv

Modified Mathlib/MeasureTheory/Measure/HasOuterApproxClosedProd.lean

Modified Mathlib/Probability/Kernel/IonescuTulcea/Maps.lean