Theorem ENNReal.prod_div_distrib_of_ne_zero

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_distrib_of_ne_zeroView on Github →