Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-17 13:06 46c42cc9

View on Github →

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.

Estimated changes

deleted def geom_sum
deleted theorem geom_sum_def
modified theorem geom_sum_one
modified theorem geom_sum_pos
modified theorem geom_sum_succ'
modified theorem geom_sum_succ
modified theorem geom_sum_two
modified theorem geom_sum_zero
deleted def geom_sum₂
deleted theorem geom_sum₂_def
deleted theorem geom_sum₂_one
modified theorem geom_sum₂_with_one
deleted theorem geom_sum₂_zero
modified theorem neg_one_geom_sum
modified theorem one_geom_sum
modified theorem zero_geom_sum
modified theorem polynomial.eval_geom_sum