Commit 2024-05-26 08:52 b6a73af0

View on Github →

chore(MeasureTheory): drop autoImplicit true (#13231)

Estimated changes

Modified Mathlib/MeasureTheory/Function/AEEqFun.lean

modified theorem MeasureTheory.AEEqFun.compMeasurePreserving_mk

modified theorem MeasureTheory.AEEqFun.compMeasurePreserving_toGerm

modified theorem MeasureTheory.AEEqFun.compQuasiMeasurePreserving_toGerm

Modified Mathlib/MeasureTheory/Function/ConditionalExpectation/AEMeasurable.lean

modified theorem MeasureTheory.AEStronglyMeasurable'.mono

Modified Mathlib/MeasureTheory/Function/LpSpace.lean

deleted theorem MeasureTheory.Memℒp.piecewise

modified theorem MeasureTheory.snorm_indicator_le