Commit 2025-08-26 23:57 29700b9f

View on Github →

feat(RingTheory): decompose archimedean classes of HahnSeries (#25970) In preparation for #25140, this connects archimedean class and HahnSeries

Estimated changes

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

added theorem toLex_eq_one

Modified Mathlib/RingTheory/HahnSeries/Basic.lean

Modified Mathlib/RingTheory/HahnSeries/Lex.lean

added theorem HahnSeries.abs_lt_abs_of_orderTop_ofLex

added theorem HahnSeries.archimedeanClassMk_eq_archimedeanClassMk_iff

added theorem HahnSeries.archimedeanClassMk_le_archimedeanClassMk_iff

added theorem HahnSeries.archimedeanClassMk_le_archimedeanClassMk_iff_of_orderTop_ofLex

added theorem HahnSeries.archimedeanClassOrderIsoWithTop_apply

added theorem HahnSeries.finiteArchimedeanClassOrderIsoLex_apply_fst

added theorem HahnSeries.finiteArchimedeanClassOrderIsoLex_apply_snd

added theorem HahnSeries.finiteArchimedeanClassOrderIso_apply