Commit 2025-08-07 17:04 7aff5e29

View on Github →

chore(GeomSum): split into ring vs field and non-ordered vs ordered parts (#26142) The motivation here is that Data.Nat.Multiplicity needs the results about geometric sums of naturals, without wanting to know anything about fields.

Estimated changes

added theorem geom_sum_Ico'
added theorem geom_sum_Ico
added theorem geom_sum_eq
added theorem geom_sum_inv
added theorem geom_sum₂_Ico
added theorem geom₂_sum
deleted theorem Commute.mul_geom_sum₂
deleted theorem Nat.geomSum_eq
deleted theorem Nat.geomSum_lt
deleted theorem Nat.geom_sum_Ico_le
deleted theorem Nat.geom_sum_le
deleted theorem Nat.pred_mul_geom_sum_le
deleted theorem Odd.add_dvd_pow_add_pow
deleted theorem Odd.geom_sum_pos
deleted theorem RingHom.map_geom_sum
deleted theorem RingHom.map_geom_sum₂
deleted theorem geom_sum_Ico'
deleted theorem geom_sum_Ico
deleted theorem geom_sum_Ico_le_of_lt_one
deleted theorem geom_sum_Ico_mul
deleted theorem geom_sum_Ico_mul_neg
deleted theorem geom_sum_eq
deleted theorem geom_sum_inv
deleted theorem geom_sum_lt
deleted theorem geom_sum_mul
deleted theorem geom_sum_mul_add
deleted theorem geom_sum_mul_neg
deleted theorem geom_sum_mul_of_le_one
deleted theorem geom_sum_mul_of_one_le
deleted theorem geom_sum_ne_zero
deleted theorem geom_sum_neg_iff
deleted theorem geom_sum_of_lt_one
deleted theorem geom_sum_of_one_lt
deleted theorem geom_sum_one
deleted theorem geom_sum_pos'
deleted theorem geom_sum_pos
deleted theorem geom_sum_pos_and_lt_one
deleted theorem geom_sum_pos_iff
deleted theorem geom_sum_succ'
deleted theorem geom_sum_succ
deleted theorem geom_sum_two
deleted theorem geom_sum_zero
deleted theorem geom_sum₂_Ico
deleted theorem geom_sum₂_comm
deleted theorem geom_sum₂_mul
deleted theorem geom_sum₂_mul_add
deleted theorem geom_sum₂_mul_of_ge
deleted theorem geom_sum₂_mul_of_le
deleted theorem geom_sum₂_self
deleted theorem geom_sum₂_succ_eq
deleted theorem geom_sum₂_with_one
deleted theorem geom₂_sum
deleted theorem geom₂_sum_of_gt
deleted theorem geom₂_sum_of_lt
deleted theorem mul_geom_sum
deleted theorem mul_geom_sum₂_Ico
deleted theorem mul_neg_geom_sum
deleted theorem nat_sub_dvd_pow_sub_pow
deleted theorem neg_one_geom_sum
deleted theorem one_geom_sum
deleted theorem one_sub_dvd_one_sub_pow
deleted theorem op_geom_sum
deleted theorem op_geom_sum₂
deleted theorem sub_dvd_pow_sub_pow
deleted theorem sub_one_dvd_pow_sub_one
deleted theorem zero_geom_sum
added theorem geom_sum_lt
added theorem geom_sum_of_lt_one
added theorem geom_sum_of_one_lt
added theorem geom₂_sum_of_gt
added theorem geom₂_sum_of_lt
added theorem Nat.geomSum_lt
added theorem Nat.geom_sum_Ico_le
added theorem Nat.geom_sum_le
added theorem Odd.geom_sum_pos
added theorem geom_sum_ne_zero
added theorem geom_sum_neg_iff
added theorem geom_sum_pos'
added theorem geom_sum_pos
added theorem geom_sum_pos_iff
added theorem Nat.geomSum_eq
added theorem RingHom.map_geom_sum
added theorem geom_sum_Ico_mul
added theorem geom_sum_Ico_mul_neg
added theorem geom_sum_mul
added theorem geom_sum_mul_add
added theorem geom_sum_mul_neg
added theorem geom_sum_mul_of_le_one
added theorem geom_sum_mul_of_one_le
added theorem geom_sum_one
added theorem geom_sum_succ'
added theorem geom_sum_succ
added theorem geom_sum_two
added theorem geom_sum_zero
added theorem geom_sum₂_comm
added theorem geom_sum₂_mul
added theorem geom_sum₂_mul_add
added theorem geom_sum₂_mul_of_ge
added theorem geom_sum₂_mul_of_le
added theorem geom_sum₂_self
added theorem geom_sum₂_succ_eq
added theorem geom_sum₂_with_one
added theorem mul_geom_sum
added theorem mul_geom_sum₂_Ico
added theorem mul_neg_geom_sum
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