Mathlib v3 is deprecated. Go to Mathlib v4

Theorem tsum_ite_eq_extract

Modification history

2023-01-19 10:30
src/topology/algebra/infinite_sum.lean
feat(topology/algebra/infinite_sum): Generalized lemmas for `add_comm_monoid` rather than `add_comm_group` (#17035) …
Deleted tsum_ite_eq_extractView on Github →
2021-06-21 03:37
src/topology/algebra/infinite_sum.lean
chore(topology/algebra/infinite_sum): small todo (#7994) …
Modified tsum_ite_eq_extractView on Github →
2021-02-04 21:33
src/topology/algebra/infinite_sum.lean
feat(topology/algebra/infinite_sum, topology/instances/ennreal): extend tsum API (#6017) …
Added tsum_ite_eq_extractView on Github →