Commit 2026-06-04 10:40 045542df

View on Github →

feat(Data/ENNReal): more big operator lemmas (#40211) Also fix the variable implicitness and and names of a few existing declarations. Renames:

coe_finsetSum to ofNNReal_finsetSum
coe_finsetProd to ofNNReal_finsetProd

Estimated changes

Modified Mathlib/Analysis/MeanInequalities.lean

Modified Mathlib/Analysis/MeanInequalitiesPow.lean

Modified Mathlib/Data/ENNReal/BigOperators.lean

deleted theorem ENNReal.coe_finsetProd

deleted theorem ENNReal.coe_finsetSum

added theorem ENNReal.ofNNReal_finsetProd

added theorem ENNReal.ofNNReal_finsetSum

added theorem ENNReal.ofNNReal_finsuppProd

added theorem ENNReal.ofNNReal_finsuppSum

modified theorem ENNReal.toNNReal_prod

modified theorem ENNReal.toReal_prod

Modified Mathlib/Data/NNReal/Basic.lean

added theorem NNReal.toReal_finsuppProd

added theorem NNReal.toReal_finsuppSum

Modified Mathlib/MeasureTheory/Measure/HasOuterApproxClosedProd.lean

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

Modified Mathlib/Topology/Algebra/InfiniteSum/ENNReal.lean