Theorem Finset.le_prod_max_one

Modification history

2026-03-03 22:45
Mathlib/Algebra/Order/BigOperators/GroupWithZero/Finset.lean
chore(Algebra/Order/BigOperators): move lemmas which don't use addition out of Ring (#35005) …
Modified Finset.le_prod_max_oneView on Github →
2026-02-16 07:36
Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean
feat(NumberTheory/Height/Basic): add bounds for sums (#34330) …
Added Finset.le_prod_max_oneView on Github →