Commit 2024-06-16 19:19 43431072

View on Github →

chore(MeasureTheory): remove remaining use of autoImplicit true (#13870)

Estimated changes

Modified Mathlib/MeasureTheory/Function/LpSpace/DomAct/Basic.lean

Modified Mathlib/MeasureTheory/Integral/FundThmCalculus.lean

Modified Mathlib/MeasureTheory/Integral/Lebesgue.lean

modified theorem MeasureTheory.lintegral_indicator_one

modified theorem MeasureTheory.lintegral_indicator_one₀

modified theorem MeasureTheory.measure_eq_top_of_lintegral_ne_top

modified theorem MeasureTheory.measure_eq_top_of_setLintegral_ne_top

modified theorem MeasureTheory.setLintegral_eq_top_of_measure_eq_top_ne_zero

Modified Mathlib/MeasureTheory/Measure/Count.lean