Commit 2021-03-25 19:35 b299d144

feat(algebra/geom_sum): rename geom_series to geom_sum, adds a lemma for the geometric sum (#6828) Declarations with names including geom_series have been renamed to use geom_sum, instead. Also adds the lemma geom_sum₂_succ_eq: geom_sum₂ x y (n + 1) = x ^ n + y * (geom_sum₂ x y n)