Commit 2025-11-24 09:57 b76ae71b

View on Github →

feat(ENNReal/BigOperators): distribute product over division in ENNReal (#32008) From the Polychromatic project.

Estimated changes

Modified Mathlib/Data/ENNReal/BigOperators.lean

modified theorem ENNReal.finsetSum_iSup

modified theorem ENNReal.finsetSum_iSup_of_monotone

added theorem ENNReal.prod_div_distrib

added theorem ENNReal.prod_div_distrib_of_ne_top

added theorem ENNReal.prod_div_distrib_of_ne_zero

modified theorem ENNReal.prod_inv_distrib