Commit 2025-11-09 13:26 26193350

View on Github →

feat(RingTheory): geometric series of (Mv)PowerSeries (#30599) Also abstracted the common part for both PowerSeries and normed rings into Summable.tsum_pow_mul_one_sub / Summable.one_sub_mul_tsum_pow.

Estimated changes

Modified Mathlib/Analysis/SpecificLimits/Normed.lean

modified theorem geom_series_mul_neg

modified theorem mul_neg_geom_series

Modified Mathlib/RingTheory/MvPowerSeries/Order.lean

added theorem MvPowerSeries.le_order_pow

added theorem MvPowerSeries.le_weightedOrder_pow

added theorem MvPowerSeries.order_ne_zero_iff_constCoeff_eq_zero

Modified Mathlib/RingTheory/MvPowerSeries/PiTopology.lean

added theorem MvPowerSeries.WithPiTopology.one_sub_mul_tsum_pow_of_constantCoeff_eq_zero

added theorem MvPowerSeries.WithPiTopology.summable_pow_of_constantCoeff_eq_zero

added theorem MvPowerSeries.WithPiTopology.tsum_pow_mul_one_sub_of_constantCoeff_eq_zero

Modified Mathlib/RingTheory/PowerSeries/Order.lean

added theorem PowerSeries.order_ne_zero_iff_constCoeff_eq_zero

Modified Mathlib/RingTheory/PowerSeries/PiTopology.lean

added theorem PowerSeries.WithPiTopology.one_sub_mul_tsum_pow_of_constantCoeff_eq_zero

added theorem PowerSeries.WithPiTopology.summable_pow_of_constantCoeff_eq_zero

added theorem PowerSeries.WithPiTopology.tsum_pow_mul_one_sub_of_constantCoeff_eq_zero

Modified Mathlib/Topology/Algebra/InfiniteSum/Ring.lean

added theorem Summable.one_sub_mul_tsum_pow

added theorem Summable.tsum_pow_mul_one_sub