Theorem hasSum_mul_left_iff

Modification history

2025-12-17 21:56
Mathlib/Topology/Algebra/InfiniteSum/Ring.lean
chore(Topology): fix whitespace (#32963) …
Modified hasSum_mul_left_iffView on Github →
2025-10-06 12:30
Mathlib/Topology/Algebra/InfiniteSum/Ring.lean
feat(Topology/Algebra/InfiniteSum): generalise to allow summation filters (#29914) …
Modified hasSum_mul_left_iffView on Github →
2024-02-29 08:53
Mathlib/Topology/Algebra/InfiniteSum/Ring.lean
chore(Topology/Algebra/InfiniteSum): split up large file (#11050) …
Modified hasSum_mul_left_iffView on Github →
2023-03-05 07:28
Mathlib/Topology/Algebra/InfiniteSum/Ring.lean
feat: Port Topology.Algebra.InfiniteSum.Ring (#2640)
Added hasSum_mul_left_iffView on Github →