Commit 2025-03-03 10:07 7b9802aa

View on Github →

chore (RingTheory/HahnSeries): rm domain hypothesis for invertibility (#22284) This PR refactors some conditions for invertibility of a Hahn series, removing the assumption that the coefficient ring is a domain and that the exponent set is a group.

Estimated changes

Modified Mathlib/RingTheory/HahnSeries/Addition.lean

added theorem HahnSeries.coeff_order_of_eq_add_single

added theorem HahnSeries.ne_zero_of_eq_add_single

added theorem HahnSeries.order_lt_order_of_eq_add_single

Modified Mathlib/RingTheory/HahnSeries/Multiplication.lean

modified theorem HahnSeries.coeff_mul_order_add_order

modified theorem HahnSeries.orderTop_add_le_mul

added theorem HahnSeries.order_mul_of_nonzero

added theorem HahnSeries.order_single_mul_of_isRegular

Modified Mathlib/RingTheory/HahnSeries/Summable.lean

added theorem HahnSeries.isUnit_of_isUnit_leadingCoeff_AddUnitOrder

added theorem HahnSeries.one_minus_single_neg_mul

modified theorem HahnSeries.unit_aux