Commit 2025-06-16 07:16 4bce37ee

View on Github →

feat(RingTheory/HahnSeries): equip HahnSeries with LinearOrder (#25168) This is part of #25140. As the future codomain of the Hahn embedding theorem, HahnSeries needs a linear order.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/RingTheory/HahnSeries/Addition.lean

added theorem HahnSeries.leadingCoeff_neg

Modified Mathlib/RingTheory/HahnSeries/Basic.lean

added theorem HahnSeries.coeff_untop_eq_leadingCoeff

Created Mathlib/RingTheory/HahnSeries/Lex.lean

added theorem HahnSeries.leadingCoeff_abs

added theorem HahnSeries.leadingCoeff_neg_iff

added theorem HahnSeries.leadingCoeff_nonneg_iff

added theorem HahnSeries.leadingCoeff_nonpos_iff

added theorem HahnSeries.leadingCoeff_pos_iff

added theorem HahnSeries.lt_iff

added theorem HahnSeries.orderTop_abs

added theorem HahnSeries.order_abs

added theorem HahnSeries.support_abs