Commit 2026-09-15 19:08 d2b0fef2

View on Github →

chore(MeasureTheory): break import cycle between QuasiMeasurePreserving and AEMeasurable (#43190) Moves QuasiMeasurePreserving.restrict and AEMeasurable.comp_quasiMeasurePreserving to the QuasiMeasurePreserving.lean file, making it possible to import the AEMeasurable.lean file from it.

Estimated changes

Modified Mathlib/Dynamics/Ergodic/MeasurePreserving.lean

Modified Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.lean

Modified Mathlib/MeasureTheory/Measure/AEMeasurable.lean

deleted theorem AEMeasurable.comp_quasiMeasurePreserving

Modified Mathlib/MeasureTheory/Measure/QuasiMeasurePreserving.lean

added theorem AEMeasurable.comp_quasiMeasurePreserving

Modified Mathlib/MeasureTheory/Measure/Restrict.lean

deleted theorem MeasureTheory.Measure.QuasiMeasurePreserving.restrict