Mathlib v3 is deprecated. Go to Mathlib v4

Theorem has_sum_fintype

Modification history

2020-06-10 09:47
src/topology/algebra/infinite_sum.lean
chore(*): use sum notation (#3014) …
Modified has_sum_fintypeView on Github →
2019-11-25 00:45
src/topology/algebra/infinite_sum.lean
feat(topology/algebra/infinite_sum): add `has_sum` versions of a few `tsum` lemmas (#1737) …
Added has_sum_fintypeView on Github →