mathlib
b299d144 - feat(algebra/geom_sum): rename geom_series to geom_sum, adds a lemma for the geometric sum (#6828)

Commit
5 years ago
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)` Co-authored-by: paulvanwamelen <30371019+paulvanwamelen@users.noreply.github.com>
Author
paulvanwamelen
Parents
Loading