Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-03-03 11:01 10848687

View on Github →

feat(analysis/{specific_limits,infinite_sum}): Cauchy of geometric bound (#753)

Estimated changes

Modified src/analysis/specific_limits.lean

added theorem cauchy_seq_of_le_geometric

Modified src/topology/algebra/infinite_sum.lean

added theorem cauchy_seq_of_has_sum_dist