Commit 2025-09-22 13:29 b4c21574

View on Github →

chore(MeasureTheory): Semilinearize integrable_comp of CLM and CLE (#29852)

Estimated changes

Modified Mathlib/MeasureTheory/Function/L1Space/Integrable.lean

modified theorem ContinuousLinearEquiv.integrable_comp_iff

modified theorem ContinuousLinearMap.integrable_comp

modified theorem LinearIsometryEquiv.integrable_comp_iff

modified theorem MeasureTheory.Integrable.apply_continuousLinearMap