Mathlib Changelog
v4
Changelog
About
Github
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