Theorem hasProd_one_iff_of_one_le

Modification history

2026-02-21 12:00
Mathlib/Topology/Algebra/InfiniteSum/Order.lean
chore: weaken `PartialOrder` to `Preorder` in `IsOrderedMonoid` hypothesis (#34295) …
Modified hasProd_one_iff_of_one_leView on Github →
2025-10-06 12:30
Mathlib/Topology/Algebra/InfiniteSum/Order.lean
feat(Topology/Algebra/InfiniteSum): generalise to allow summation filters (#29914) …
Modified hasProd_one_iff_of_one_leView on Github →
2024-03-30 22:01
Mathlib/Topology/Algebra/InfiniteSum/Order.lean
feat: Infinite products (#11733) …
Added hasProd_one_iff_of_one_leView on Github →