Theorem Finset.one_le_prod

Modification history

2026-03-05 14:29
Mathlib/Algebra/Order/BigOperators/GroupWithZero/Finset.lean
feat(Algebra/Order/BigOperators): order properties of subsets in groups with zero (#35008) …
Modified Finset.one_le_prodView on Github →
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.one_le_prodView on Github →
2026-01-05 16:12
Mathlib/Algebra/Order/BigOperators/GroupWithZero/Finset.lean
feat(NumberTheory/Height/Basic): first installment of heights (#33054) …
Added Finset.one_le_prodView on Github →