Theorem Finset.mulLECancellable_prod

Modification history

2024-10-01 20:15
Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
feat(ENNReal): Convenience lemmas (#17277) …
Added Finset.mulLECancellable_prodView on Github →