Lexicographical order on Hahn series

In this file, we define lexicographical ordered Lex (HahnSeries Γ R), and show this is a LinearOrder when Γ and R themselves are linearly ordered. Additionally, it is an ordered group when R is.

instance HahnSeries.instPartialOrderLex {Γ : Type u_1} {R : Type u_2} [LinearOrder Γ] [Zero R] [PartialOrder R] : PartialOrder (Lex (HahnSeries Γ R))

Equations

• HahnSeries.instPartialOrderLex = PartialOrder.lift (fun (x : Lex (HahnSeries Γ R)) => toLex (ofLex x).coeff) ⋯

theorem HahnSeries.lt_iff {Γ : Type u_1} {R : Type u_2} [LinearOrder Γ] [Zero R] [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

noncomputable instance HahnSeries.instLinearOrderLex {Γ : Type u_1} {R : Type u_2} [LinearOrder Γ] [Zero R] [LinearOrder R] : LinearOrder (Lex (HahnSeries Γ R))

Equations

• One or more equations did not get rendered due to their size.

theorem HahnSeries.leadingCoeff_pos_iff {Γ : Type u_1} {R : Type u_2} [LinearOrder Γ] [Zero R] [LinearOrder R] {x : Lex (HahnSeries Γ R)} : 0 < (ofLex x).leadingCoeff ↔ 0 < x

theorem HahnSeries.leadingCoeff_nonneg_iff {Γ : Type u_1} {R : Type u_2} [LinearOrder Γ] [Zero R] [LinearOrder R] {x : Lex (HahnSeries Γ R)} : 0 ≤ (ofLex x).leadingCoeff ↔ 0 ≤ x

theorem HahnSeries.leadingCoeff_neg_iff {Γ : Type u_1} {R : Type u_2} [LinearOrder Γ] [Zero R] [LinearOrder R] {x : Lex (HahnSeries Γ R)} : (ofLex x).leadingCoeff < 0 ↔ x < 0

theorem HahnSeries.leadingCoeff_nonpos_iff {Γ : Type u_1} {R : Type u_2} [LinearOrder Γ] [Zero R] [LinearOrder R] {x : Lex (HahnSeries Γ R)} : (ofLex x).leadingCoeff ≤ 0 ↔ x ≤ 0

instance HahnSeries.instIsOrderedAddMonoidLex {Γ : Type u_1} {R : Type u_2} [LinearOrder Γ] [PartialOrder R] [AddCommMonoid R] [AddLeftStrictMono R] : IsOrderedAddMonoid (Lex (HahnSeries Γ R))

theorem HahnSeries.support_abs {Γ : Type u_1} {R : Type u_2} [LinearOrder Γ] [LinearOrder R] [AddCommGroup R] [IsOrderedAddMonoid R] (x : Lex (HahnSeries Γ R)) : (ofLex |x|).support = (ofLex x).support

theorem HahnSeries.orderTop_abs {Γ : Type u_1} {R : Type u_2} [LinearOrder Γ] [LinearOrder R] [AddCommGroup R] [IsOrderedAddMonoid R] (x : Lex (HahnSeries Γ R)) : (ofLex |x|).orderTop = (ofLex x).orderTop

theorem HahnSeries.order_abs {Γ : Type u_1} {R : Type u_2} [LinearOrder Γ] [LinearOrder R] [AddCommGroup R] [IsOrderedAddMonoid R] [Zero Γ] (x : Lex (HahnSeries Γ R)) : (ofLex |x|).order = (ofLex x).order

theorem HahnSeries.leadingCoeff_abs {Γ : Type u_1} {R : Type u_2} [LinearOrder Γ] [LinearOrder R] [AddCommGroup R] [IsOrderedAddMonoid R] (x : Lex (HahnSeries Γ R)) : (ofLex |x|).leadingCoeff = |(ofLex x).leadingCoeff|