Commit 2025-11-24 08:57 ee4aed76

View on Github →

feat (RingTheory/HahnSeries): introduce binomialFamily and generalized powers. (#31215) We introduce a way to take generalized powers of Hahn series whose leading term is 1. The powers take values in a binomial ring.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/RingTheory/HahnSeries/Addition.lean

added theorem HahnSeries.le_orderTop_of_leadingCoeff_eq

added theorem HahnSeries.orderTop_le_orderTop_smul

added theorem HahnSeries.orderTop_sub_ne

Modified Mathlib/RingTheory/HahnSeries/Basic.lean

added theorem HahnSeries.orderTop_ne_of_coeff_eq_zero

Created Mathlib/RingTheory/HahnSeries/Binomial.lean

added def HahnSeries.SummableFamily.binomialFamily

added theorem HahnSeries.SummableFamily.binomialFamily_apply

added theorem HahnSeries.SummableFamily.binomialFamily_apply_of_orderTop_nonpos

added theorem HahnSeries.SummableFamily.binomialFamily_mem_support

added theorem HahnSeries.SummableFamily.binomialFamily_orderTop_pos

added theorem HahnSeries.SummableFamily.orderTop_hsum_binomialFamily_pos

added theorem HahnSeries.binomial_power

added theorem HahnSeries.coeff_toOrderTopSubOnePos_pow

added theorem HahnSeries.pow_add

Modified Mathlib/RingTheory/HahnSeries/Multiplication.lean

added theorem HahnSeries.leadingCoeff_mul_of_nonzero

added theorem HahnSeries.mem_orderTopSubOnePos_iff

added def HahnSeries.orderTopSubOnePos

added theorem HahnSeries.orderTop_mul_of_nonzero

modified theorem HahnSeries.orderTop_nsmul_le_orderTop_pow

modified theorem HahnSeries.orderTop_one

added theorem HahnSeries.orderTop_self_sub_one_pos_iff

added theorem HahnSeries.orderTop_sub_pos

Modified Mathlib/RingTheory/HahnSeries/Summable.lean

added theorem HahnSeries.SummableFamily.hsum_leadingCoeff_of_le

added theorem HahnSeries.SummableFamily.hsum_orderTop_of_le

added theorem HahnSeries.SummableFamily.le_hsum_support_mem

added theorem HahnSeries.isUnit_of_orderTop_pos

added def HahnSeries.toOrderTopSubOnePos