Mathlib v3 is deprecated. Go to Mathlib v4

Theorem dist_partial_sum_le_of_le_geometric

Modification history

2022-11-17 13:13
src/analysis/specific_limits/normed.lean
refactor(analysis): change the symbol for norm to align with the unicode spec (#17575) …
Modified dist_partial_sum_le_of_le_geometricView on Github →
2020-03-18 23:51
src/analysis/specific_limits.lean
feat(topology/algebra/infinite_sum): dot notation, cauchy sequences (#2171) …
Added dist_partial_sum_le_of_le_geometricView on Github →