Theorem multipliable_iff_cauchySeq_finset

Modification history

2026-03-04 18:05
Mathlib/Topology/Algebra/InfiniteSum/Group.lean
chore(Topology/Algebra/InfiniteSum/Group): generalize the Cauchy criterion to `CommMonoid` (#36138) …
Modified multipliable_iff_cauchySeq_finsetView on Github →
2024-03-30 22:01
Mathlib/Topology/Algebra/InfiniteSum/Group.lean
feat: Infinite products (#11733) …
Added multipliable_iff_cauchySeq_finsetView on Github →