Mathlib v3 is deprecated. Go to Mathlib v4

Theorem has_sum_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 has_sum_ite_eq_extractView on Github →
2021-06-21 03:37
src/topology/algebra/infinite_sum.lean
chore(topology/algebra/infinite_sum): small todo (#7994) …
Added has_sum_ite_eq_extractView on Github →