Theorem Finset.le_prod_max_one

Modification history

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 →