Mathlib v3 is deprecated. Go to Mathlib v4

Theorem cauchy_seq_of_has_sum_dist

Modification history

2019-04-10 17:14
src/topology/algebra/infinite_sum.lean
rename has_sum and is_sum to summable and has_sum (#912)
Deleted cauchy_seq_of_has_sum_distView on Github →
2019-03-03 11:01
src/topology/algebra/infinite_sum.lean
feat(analysis/{specific_limits,infinite_sum}): Cauchy of geometric bound (#753)
Added cauchy_seq_of_has_sum_distView on Github →