Theorem Finset.prod_image_le_of_one_le

Modification history

2025-10-09 08:14
Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
chore(Algebra/Order/BigOperators/Group/{Finset, Multiset}): generalize results to `(Mul)(Add)LeftMono` (#29864) …
Modified Finset.prod_image_le_of_one_leView on Github →
2025-02-03 09:44
Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
(sub-)additivity of an addContent on a (semi-)ring of sets (#21036) …
Added Finset.prod_image_le_of_one_leView on Github →