Commit 2025-08-19 23:16 8bb991a4

View on Github →

chore(HahnSeries): make more usable, golf (#28632) A lot of lemmas were misnamed or the wrong way around.

Estimated changes

Modified Mathlib/Algebra/Order/Group/Synonym.lean

added theorem ofLex_eq_one

Modified Mathlib/Order/WithBot.lean

modified theorem WithTop.lt_untop_iff

modified theorem WithTop.untop_lt_iff

Modified Mathlib/RingTheory/HahnSeries/Addition.lean

modified def HahnSeries.addOppositeEquiv

modified theorem HahnSeries.addOppositeEquiv_leadingCoeff

modified theorem HahnSeries.addOppositeEquiv_orderTop

modified theorem HahnSeries.addOppositeEquiv_support

Modified Mathlib/RingTheory/HahnSeries/Basic.lean

modified theorem HahnSeries.coeff_untop_eq_leadingCoeff

modified def HahnSeries.leadingCoeff

deleted theorem HahnSeries.leadingCoeff_eq_iff

added theorem HahnSeries.leadingCoeff_eq_zero

deleted theorem HahnSeries.leadingCoeff_ne_iff

added theorem HahnSeries.leadingCoeff_ne_zero

deleted theorem HahnSeries.leadingCoeff_of_ne

added theorem HahnSeries.leadingCoeff_of_ne_zero

modified theorem HahnSeries.leadingCoeff_zero

modified theorem HahnSeries.ne_zero_iff_orderTop

added theorem HahnSeries.orderTop_eq_top

deleted theorem HahnSeries.orderTop_eq_top_iff

added theorem HahnSeries.orderTop_lt_top

added theorem HahnSeries.orderTop_ne_top

deleted theorem HahnSeries.orderTop_of_Subsingleton

deleted theorem HahnSeries.orderTop_of_ne

added theorem HahnSeries.orderTop_of_ne_zero

added theorem HahnSeries.orderTop_of_subsingleton

deleted theorem HahnSeries.order_eq_orderTop_of_ne

added theorem HahnSeries.order_eq_orderTop_of_ne_zero

Modified Mathlib/RingTheory/HahnSeries/Lex.lean

Modified Mathlib/RingTheory/HahnSeries/Multiplication.lean

Modified Mathlib/RingTheory/HahnSeries/Summable.lean

Modified Mathlib/RingTheory/HahnSeries/Valuation.lean