mathlib3

00d9f1de - feat(topology/algebra/infinite_sum): dot notation, cauchy sequences (#2171)

feat(topology/algebra/infinite_sum): dot notation, cauchy sequences (#2171) * more material on infinite sums * minor fixes * cleanup * yury's comments Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>