Theorem tsum_congr_cofinite₀

Modification history

2025-04-13 16:12
Mathlib/Topology/Algebra/InfiniteSum/Group.lean
chore(tprod): move tprod lemmas to protected namespace (#23959) …
Deleted tsum_congr_cofinite₀View on Github →
2025-04-08 15:48
Mathlib/Topology/Algebra/InfiniteSum/Group.lean
feat(Topology/Algebra/InfiniteSum): lemmas about tprods in a GroupWithZero (#23803) …
Added tsum_congr_cofinite₀View on Github →