Commit 2023-01-29 16:43 2efb2c6f

View on Github →

feat: port Algebra.GeomSum (#1922)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/GeomSum.lean

added theorem Commute.mul_geom_sum₂

added theorem Commute.mul_neg_geom_sum₂

added theorem Nat.geom_sum_Ico_le

added theorem Nat.geom_sum_le

added theorem Nat.pred_mul_geom_sum_le

added theorem Odd.add_dvd_pow_add_pow

added theorem Odd.geom_sum_pos

added theorem Odd.nat_add_dvd_pow_add_pow

added theorem RingHom.map_geom_sum

added theorem RingHom.map_geom_sum₂

added theorem geom_sum_Ico'

added theorem geom_sum_Ico

added theorem geom_sum_Ico_le_of_lt_one

added theorem geom_sum_Ico_mul

added theorem geom_sum_Ico_mul_neg

added theorem geom_sum_alternating_of_le_neg_one

added theorem geom_sum_alternating_of_lt_neg_one

added theorem geom_sum_eq

added theorem geom_sum_eq_zero_iff_neg_one

added theorem geom_sum_inv

added theorem geom_sum_mul

added theorem geom_sum_mul_add

added theorem geom_sum_mul_neg

added theorem geom_sum_ne_zero

added theorem geom_sum_neg_iff

added theorem geom_sum_one

added theorem geom_sum_pos'

added theorem geom_sum_pos

added theorem geom_sum_pos_and_lt_one

added theorem geom_sum_pos_iff

added theorem geom_sum_succ'

added theorem geom_sum_succ

added theorem geom_sum_two

added theorem geom_sum_zero

added theorem geom_sum₂_Ico

added theorem geom_sum₂_comm

added theorem geom_sum₂_mul

added theorem geom_sum₂_mul_add

added theorem geom_sum₂_self

added theorem geom_sum₂_succ_eq

added theorem geom_sum₂_with_one

added theorem geom₂_sum

added theorem mul_geom_sum

added theorem mul_geom_sum₂_Ico

added theorem mul_neg_geom_sum

added theorem nat_sub_dvd_pow_sub_pow

added theorem neg_one_geom_sum

added theorem one_geom_sum

added theorem op_geom_sum

added theorem op_geom_sum₂

added theorem sub_dvd_pow_sub_pow

added theorem zero_geom_sum