Theorems · Theorem · order theory

HahnSeries.lt_iff

∀ {Γ : Type u_1} {R : Type u_2} [inst : LinearOrder Γ] [inst_1 : Zero R] [inst_2 : PartialOrder R]
  (a b : Lex (HahnSeries Γ R)),
  a < b ↔ ∃ i, (∀ j < i, (ofLex a).coeff j = (ofLex b).coeff j) ∧ (ofLex a).coeff i < (ofLex b).coeff i

Defined in

Mathlib.RingTheory.HahnSeries.Lex

Cited by

5 results in Mathlib

Foundations

Depth 21 from the axioms · uses propext, Quot.sound

Assumes

LinearOrderZeroPartialOrder