mathlib

d2d29ffd - feat(algebra/geom_sum): sum of a geom_series over an Ico (#1573)

feat(algebra/geom_sum): sum of a geom_series over an Ico (#1573) * feat(algebra/geom_sum): sum of a geom_series over an Ico * Add two more versions as requested by @jcommelin