Theorem tsum_zero'

Modification history

2023-07-16 14:44

Mathlib/Topology/Algebra/InfiniteSum/Basic.lean

feat(Topology.Algebra.InfiniteSum): make sure that tsum and sum coincide on fintypes (#5914) …

Deleted tsum_zero'View on Github →

2023-07-02 10:21

Mathlib/Topology/Algebra/InfiniteSum/Basic.lean

fix: `∑'` precedence (#5615) …

Modified tsum_zero'View on Github →

2023-06-04 14:19

Mathlib/Topology/Algebra/InfiniteSum/Basic.lean

style: allow `_` for an argument in `notation3` & replace `_foo` with `_` in `notation3` (#4652)

Modified tsum_zero'View on Github →

2023-03-02 07:55

Mathlib/Topology/Algebra/InfiniteSum/Basic.lean

feat: port Topology.Algebra.InfiniteSum.Basic (#2500)

Added tsum_zero'View on Github →