Theorem ENNReal.prod_div_distrib

Modification history

2025-11-24 09:57
Mathlib/Data/ENNReal/BigOperators.lean
feat(ENNReal/BigOperators): distribute product over division in ENNReal (#32008) …
Added ENNReal.prod_div_distribView on Github →