Commit 2026-01-02 13:48 f668f459

View on Github →

feat: cardinality of Hahn series inverse (#32643)

Estimated changes

Modified Mathlib/RingTheory/HahnSeries/Addition.lean

Modified Mathlib/RingTheory/HahnSeries/Basic.lean

added theorem HahnSeries.coeff_order_eq_zero

modified theorem HahnSeries.coeff_order_ne_zero

Modified Mathlib/RingTheory/HahnSeries/Cardinal.lean

added theorem HahnSeries.cardSupp_div_le

added theorem HahnSeries.cardSupp_hsum_le

added theorem HahnSeries.cardSupp_hsum_powers_le

added theorem HahnSeries.cardSupp_inv_le

added theorem HahnSeries.cardSupp_mul_single_le

added theorem HahnSeries.cardSupp_one

added theorem HahnSeries.cardSupp_one_le

added theorem HahnSeries.cardSupp_pow_le

added theorem HahnSeries.cardSupp_single_mul_le

Modified Mathlib/RingTheory/HahnSeries/Multiplication.lean

added theorem HahnSeries.coeff_mul_single

added theorem HahnSeries.coeff_single_mul

Modified Mathlib/RingTheory/LaurentSeries.lean