Theorems · Theorem · order theory

HahnSeries.archimedeanClassMk_le_archimedeanClassMk_iff

∀ {Γ : Type u_1} {R : Type u_2} [inst : LinearOrder Γ] [inst_1 : LinearOrder R] [inst_2 : AddCommGroup R]
  [inst_3 : IsOrderedAddMonoid R] {x y : Lex (HahnSeries Γ R)},
  ArchimedeanClass.mk x ≤ ArchimedeanClass.mk y ↔
    (ofLex x).orderTop < (ofLex y).orderTop ∨
      (ofLex x).orderTop = (ofLex y).orderTop ∧
        ArchimedeanClass.mk (ofLex x).leadingCoeff ≤ ArchimedeanClass.mk (ofLex y).leadingCoeff

Defined in

Mathlib.RingTheory.HahnSeries.Lex

Cited by

1 results in Mathlib

Foundations

Depth 110 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

LinearOrderLinearOrderAddCommGroupIsOrderedAddMonoid