Commit 2026-10-21 09:51 c31114ff

View on Github →

feat: use IsApply for SimpleFunc (#45077)

Estimated changes

Modified Mathlib/Analysis/Fourier/PoissonSummation.lean

Modified Mathlib/Analysis/SpecialFunctions/MulExpNegMulSqIntegral.lean

Modified Mathlib/Geometry/Euclidean/Volume/Measure.lean

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

Modified Mathlib/MeasureTheory/Function/SimpleFunc.lean

deleted theorem MeasureTheory.SimpleFunc.coe_div

deleted theorem MeasureTheory.SimpleFunc.coe_intCast

deleted theorem MeasureTheory.SimpleFunc.coe_inv

deleted theorem MeasureTheory.SimpleFunc.coe_mul

deleted theorem MeasureTheory.SimpleFunc.coe_natCast

deleted theorem MeasureTheory.SimpleFunc.coe_one

deleted theorem MeasureTheory.SimpleFunc.coe_pow

deleted theorem MeasureTheory.SimpleFunc.coe_smul

deleted theorem MeasureTheory.SimpleFunc.coe_zpow

deleted theorem MeasureTheory.SimpleFunc.div_apply

deleted theorem MeasureTheory.SimpleFunc.inv_apply

deleted theorem MeasureTheory.SimpleFunc.mul_apply

deleted theorem MeasureTheory.SimpleFunc.pow_apply

deleted theorem MeasureTheory.SimpleFunc.smul_apply

deleted theorem MeasureTheory.SimpleFunc.zpow_apply

Modified Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean

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

Modified Mathlib/MeasureTheory/Integral/Bochner/L1.lean

Modified Mathlib/MeasureTheory/Integral/Bochner/Set.lean

Modified Mathlib/MeasureTheory/Integral/Bochner/VitaliCaratheodory.lean

Modified Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean

Modified Mathlib/MeasureTheory/Integral/Lebesgue/Add.lean

Modified Mathlib/MeasureTheory/Integral/Lebesgue/Basic.lean

Modified Mathlib/MeasureTheory/Integral/Lebesgue/Countable.lean

Modified Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean

Modified Mathlib/NumberTheory/NumberField/CanonicalEmbedding/NormLeOne.lean

Modified Mathlib/Probability/Kernel/Composition/CompProd.lean

Modified Mathlib/Probability/Kernel/MeasurableLIntegral.lean

Modified Mathlib/Probability/StrongLaw.lean