refactor(algebra/geom_sum): remove definition (#14120)
There's no need to have a separate definition `geom_sum := ∑ i in range n, x ^ i`. Instead it's better to just write the lemmas about the sum itself: that way `simp` lemmas fire "in the wild", without needing to rewrite expression in terms of `geom_sum` manually.
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
