Nimber polynomials

This file contains multiple auxiliary results and definitions for working with nimber polynomials:

• IsField.embed: embeds a polynomial p : Nimber[X] into the subfield Iio x, for IsField x.
• Lex.instLinearOrderPolynomial: a linear order instance on nimber polynomials, defined as the colexicographic ordering.
• leastNoRoots x: the smallest non-constant polynomial in x without roots less than x.

For Mathlib

theorem Polynomial.natDegree_eq_zero_iff {R : Type u_1} [Semiring R] {p : Polynomial R} : p.natDegree = 0 ↔ p = 0 ∨ p.degree = 0

theorem Polynomial.self_sub_X_pow_of_monic {R : Type u_2} [Ring R] {p : Polynomial R} (h : p.Monic) : p - X ^ p.natDegree = p.eraseLead

theorem Polynomial.degree_pos_of_mem_roots {R : Type u_2} [CommRing R] [IsDomain R] {p : Polynomial R} {r : R} (h : r ∈ p.roots) : 0 < p.degree

theorem Polynomial.monomial_induction {R : Type u_1} [Semiring R] {motive : Polynomial R → Prop} (zero : motive 0) (add : ∀ (a : R) (n : ℕ) (q : Polynomial R), q.degree < ↑n → motive q → motive (C a * X ^ n + q)) (p : Polynomial R) : motive p

theorem Polynomial.eq_add_C_mul_X_pow_of_degree_le {R : Type u_1} [Semiring R] {p : Polynomial R} {n : ℕ} (h : p.degree ≤ ↑n) : ∃ (a : R) (q : Polynomial R), p = q + C a * X ^ n ∧ q.degree < ↑n

theorem WithBot.le_zero_iff {α : Type u_1} [AddZeroClass α] [PartialOrder α] [CanonicallyOrderedAdd α] {x : WithBot α} : x ≤ 0 ↔ x = ⊥ ∨ x = 0

theorem WithBot.coe_add_one (n : ℕ) : ↑(n + 1) = ↑n + 1

@[simp]

theorem WithBot.natCast_eq_coe (n : ℕ) : ↑n = ↑n

@[simp]

theorem WithBot.lt_add_one {x : WithBot ℕ} (n : ℕ) : x < ↑n + 1 ↔ x ≤ ↑n

theorem WithBot.add_pos_of_pos_of_nonneg {α : Type u_1} [AddZeroClass α] [Preorder α] [AddLeftMono α] {a b : WithBot α} (ha : 0 < a) (hb : 0 ≤ b) : 0 < a + b

@[simp]

theorem WithBot.succ_one' : Order.succ 1 = 2

theorem WithTop.untop_eq {α : Type u_1} {x : WithTop α} {y : α} (h : x = ↑y) : x.untop ⋯ = y

theorem WithTop.eq_untop {α : Type u_1} {x : WithTop α} {y : α} (h : ↑y = x) : y = x.untop ⋯

Basic results

theorem Nimber.polynomial_eq_zero_of_le_one {x : Nimber} {p : Polynomial Nimber} (hx₁ : x ≤ 1) (h : ∀ (k : ℕ), p.coeff k < x) : p = 0

theorem Nimber.IsRing.eval_lt {x y : Nimber} (h : x.IsRing) {p : Polynomial Nimber} (hp : ∀ (k : ℕ), p.coeff k < x) (hy : y < x) : Polynomial.eval y p < x

theorem Nimber.coeff_X_pow_lt {x : Nimber} (n : ℕ) (h : 1 < x) (k : ℕ) : (Polynomial.X ^ n).coeff k < x

theorem Nimber.coeff_X_lt {x : Nimber} (h : 1 < x) (k : ℕ) : Polynomial.X.coeff k < x

theorem Nimber.IsGroup.coeff_add_lt {x : Nimber} {p q : Polynomial Nimber} (h : x.IsGroup) (hp : ∀ (k : ℕ), p.coeff k < x) (hq : ∀ (k : ℕ), q.coeff k < x) (k : ℕ) : (p + q).coeff k < x

theorem Nimber.IsGroup.coeff_sum_lt {x : Nimber} {ι : Type u_2} {f : ι → Polynomial Nimber} {s : Finset ι} (h : x.IsGroup) (hs : ∀ y ∈ s, ∀ (k : ℕ), (f y).coeff k < x) (k : ℕ) : (s.sum f).coeff k < x

theorem Nimber.coeff_zero_lt {x : Nimber} (h : x ≠ 0) (k : ℕ) : (Polynomial.coeff 0) k < x

theorem Nimber.IsRing.coeff_mul_lt {x : Nimber} {p q : Polynomial Nimber} (h : x.IsRing) (hp : ∀ (k : ℕ), p.coeff k < x) (hq : ∀ (k : ℕ), q.coeff k < x) (k : ℕ) : (p * q).coeff k < x

theorem Nimber.IsRing.coeff_prod_lt {x : Nimber} {ι : Type u_2} {f : ι → Polynomial Nimber} {s : Finset ι} (h : x.IsRing) (hs : ∀ y ∈ s, ∀ (k : ℕ), (f y).coeff k < x) (k : ℕ) : (s.prod f).coeff k < x

theorem Nimber.coeff_one_lt {x : Nimber} (h : 1 < x) (k : ℕ) : (Polynomial.coeff 1) k < x

theorem Nimber.coeff_C_lt {x y : Nimber} (h : y < x) (k : ℕ) : (Polynomial.C y).coeff k < x

Embedding in a subfield

noncomputable def Nimber.IsField.embed {x : Nimber} (h : x.IsField) (p : Polynomial Nimber) (hp : ∀ (k : ℕ), p.coeff k < x) : Polynomial ↥h.toSubfield

Reinterpret a polynomial in the nimbers as a polynomial in the subfield x.

We could define this under the weaker assumption IsRing, but due to proof erasure, this leads to issues where Field (h.toSubring ⋯) can't be inferred, even if h : IsField x.

Equations

• h.embed p hp = { toFinsupp := AddMonoidAlgebra.ofCoeff { support := p.support, toFun := fun (k : ℕ) => ⟨p.coeff k, ⋯⟩, mem_support_toFun := ⋯ } }

@[simp]

theorem Nimber.IsField.coeff_embed {x : Nimber} (h : x.IsField) {p : Polynomial Nimber} (hp : ∀ (k : ℕ), p.coeff k < x) (k : ℕ) : (h.embed p hp).coeff k = ⟨p.coeff k, ⋯⟩

@[simp]

theorem Nimber.IsField.degree_embed {x : Nimber} (h : x.IsField) {p : Polynomial Nimber} (hp : ∀ (k : ℕ), p.coeff k < x) : (h.embed p hp).degree = p.degree

@[simp]

theorem Nimber.IsField.leadingCoeff_embed {x : Nimber} (h : x.IsField) {p : Polynomial Nimber} (hp : ∀ (k : ℕ), p.coeff k < x) : (h.embed p hp).leadingCoeff = ⟨p.leadingCoeff, ⋯⟩

@[simp]

theorem Nimber.IsField.monic_embed {x : Nimber} (h : x.IsField) {p : Polynomial Nimber} (hp : ∀ (k : ℕ), p.coeff k < x) : (h.embed p hp).Monic ↔ p.Monic

@[simp]

theorem Nimber.IsField.map_embed {x : Nimber} (h : x.IsField) {p : Polynomial Nimber} (hp : ∀ (k : ℕ), p.coeff k < x) : Polynomial.map h.toSubfield.subtype (h.embed p hp) = p

@[simp]

theorem Nimber.IsField.embed_C {x : Nimber} (h : x.IsField) {y : Nimber} {hy : ∀ (k : ℕ), (Polynomial.C y).coeff k < x} : h.embed (Polynomial.C y) hy = Polynomial.C ⟨y, ⋯⟩

@[simp]

theorem Nimber.IsField.eval_embed {x : Nimber} (h : x.IsField) {p : Polynomial Nimber} (hp : ∀ (k : ℕ), p.coeff k < x) (y : ↥h.toSubfield) : Polynomial.eval y (h.embed p hp) = ⟨Polynomial.eval (↑y) p, ⋯⟩

Lexicographic ordering on polynomials

@[instance_reducible]

noncomputable instance Nimber.Lex.instLinearOrderPolynomial : LinearOrder (Polynomial Nimber)

The colexicographic ordering on nimber polynomials.

Equations

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

theorem Nimber.Lex.lt_def {p q : Polynomial Nimber} : p < q ↔ ∃ (n : ℕ), (∀ (k : ℕ), n < k → p.coeff k = q.coeff k) ∧ p.coeff n < q.coeff n

instance Nimber.Lex.instWellFoundedLTPolynomial : WellFoundedLT (Polynomial Nimber)

@[instance_reducible]

noncomputable instance Nimber.Lex.instOrderBotPolynomial : OrderBot (Polynomial Nimber)

Equations

• Nimber.Lex.instOrderBotPolynomial = { bot := 0, bot_le := ⋯ }

@[simp]

theorem Nimber.Lex.bot_eq_zero : ⊥ = 0

@[simp]

theorem Nimber.Lex.le_zero_iff {p : Polynomial Nimber} : p ≤ 0 ↔ p = 0

@[instance_reducible]

noncomputable instance Nimber.Lex.instConditionallyCompleteLinearOrderBotPolynomial : ConditionallyCompleteLinearOrderBot (Polynomial Nimber)

Equations

• Nimber.Lex.instConditionallyCompleteLinearOrderBotPolynomial = WellFoundedLT.conditionallyCompleteLinearOrderBot (Polynomial Nimber)

theorem Nimber.Lex.forall_lt_quadratic {P : Polynomial Nimber → Prop} {x y z : Nimber} : (∀ p < Polynomial.C x * Polynomial.X ^ 2 + Polynomial.C y * Polynomial.X + Polynomial.C z, P p) ↔ (∀ c < z, P (Polynomial.C x * Polynomial.X ^ 2 + Polynomial.C y * Polynomial.X + Polynomial.C c)) ∧ (∀ b < y, ∀ (c : Nimber), P (Polynomial.C x * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c)) ∧ ∀ a < x, ∀ (b c : Nimber), P (Polynomial.C a * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c)

theorem Nimber.Lex.forall_le_quadratic {P : Polynomial Nimber → Prop} {x y z : Nimber} : (∀ p ≤ Polynomial.C x * Polynomial.X ^ 2 + Polynomial.C y * Polynomial.X + Polynomial.C z, P p) ↔ (∀ c ≤ z, P (Polynomial.C x * Polynomial.X ^ 2 + Polynomial.C y * Polynomial.X + Polynomial.C c)) ∧ (∀ b < y, ∀ (c : Nimber), P (Polynomial.C x * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c)) ∧ ∀ a < x, ∀ (b c : Nimber), P (Polynomial.C a * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c)

theorem Nimber.Lex.exists_lt_quadratic {P : Polynomial Nimber → Prop} {x y z : Nimber} : (∃ p < Polynomial.C x * Polynomial.X ^ 2 + Polynomial.C y * Polynomial.X + Polynomial.C z, P p) ↔ (∃ c < z, P (Polynomial.C x * Polynomial.X ^ 2 + Polynomial.C y * Polynomial.X + Polynomial.C c)) ∨ (∃ b < y, ∃ (c : Nimber), P (Polynomial.C x * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c)) ∨ ∃ a < x, ∃ (b : Nimber) (c : Nimber), P (Polynomial.C a * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c)

theorem Nimber.Lex.exists_le_quadratic {P : Polynomial Nimber → Prop} {x y z : Nimber} : (∃ p ≤ Polynomial.C x * Polynomial.X ^ 2 + Polynomial.C y * Polynomial.X + Polynomial.C z, P p) ↔ (∃ c ≤ z, P (Polynomial.C x * Polynomial.X ^ 2 + Polynomial.C y * Polynomial.X + Polynomial.C c)) ∨ (∃ b < y, ∃ (c : Nimber), P (Polynomial.C x * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c)) ∨ ∃ a < x, ∃ (b : Nimber) (c : Nimber), P (Polynomial.C a * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c)

theorem Nimber.Lex.forall_lt_linear {P : Polynomial Nimber → Prop} {x y : Nimber} : (∀ p < Polynomial.C x * Polynomial.X + Polynomial.C y, P p) ↔ (∀ b < y, P (Polynomial.C x * Polynomial.X + Polynomial.C b)) ∧ ∀ a < x, ∀ (b : Nimber), P (Polynomial.C a * Polynomial.X + Polynomial.C b)

theorem Nimber.Lex.forall_le_linear {P : Polynomial Nimber → Prop} {x y : Nimber} : (∀ p ≤ Polynomial.C x * Polynomial.X + Polynomial.C y, P p) ↔ (∀ b ≤ y, P (Polynomial.C x * Polynomial.X + Polynomial.C b)) ∧ ∀ a < x, ∀ (b : Nimber), P (Polynomial.C a * Polynomial.X + Polynomial.C b)

theorem Nimber.Lex.exists_lt_linear {P : Polynomial Nimber → Prop} {x y : Nimber} : (∃ p < Polynomial.C x * Polynomial.X + Polynomial.C y, P p) ↔ (∃ b < y, P (Polynomial.C x * Polynomial.X + Polynomial.C b)) ∨ ∃ a < x, ∃ (b : Nimber), P (Polynomial.C a * Polynomial.X + Polynomial.C b)

theorem Nimber.Lex.exists_le_linear {P : Polynomial Nimber → Prop} {x y : Nimber} : (∃ p ≤ Polynomial.C x * Polynomial.X + Polynomial.C y, P p) ↔ (∃ b ≤ y, P (Polynomial.C x * Polynomial.X + Polynomial.C b)) ∨ ∃ a < x, ∃ (b : Nimber), P (Polynomial.C a * Polynomial.X + Polynomial.C b)

@[simp]

theorem Nimber.Lex.forall_lt_C {P : Polynomial Nimber → Prop} {x : Nimber} : (∀ p < Polynomial.C x, P p) ↔ ∀ a < x, P (Polynomial.C a)

@[simp]

theorem Nimber.Lex.forall_le_C {P : Polynomial Nimber → Prop} {x : Nimber} : (∀ y ≤ Polynomial.C x, P y) ↔ ∀ y ≤ x, P (Polynomial.C y)

@[simp]

theorem Nimber.Lex.exists_lt_C {P : Polynomial Nimber → Prop} {x : Nimber} : (∃ y < Polynomial.C x, P y) ↔ ∃ y < x, P (Polynomial.C y)

@[simp]

theorem Nimber.Lex.exists_le_C {P : Polynomial Nimber → Prop} {x : Nimber} : (∃ y ≤ Polynomial.C x, P y) ↔ ∃ y ≤ x, P (Polynomial.C y)

theorem Nimber.Lex.degree_mono : Monotone Polynomial.degree

theorem Nimber.Lex.natDegree_mono : Monotone Polynomial.natDegree

theorem Nimber.Lex.C_strictMono : StrictMono ⇑Polynomial.C

@[simp]

theorem Nimber.Lex.C_lt_C_iff {x y : Nimber} : Polynomial.C x < Polynomial.C y ↔ x < y

@[simp]

theorem Nimber.Lex.C_le_C_iff {x y : Nimber} : Polynomial.C x ≤ Polynomial.C y ↔ x ≤ y

theorem Nimber.Lex.lt_of_degree_lt {p q : Polynomial Nimber} (h : p.degree < q.degree) : p < q

theorem Nimber.Lex.lt_of_natDegree_lt {p q : Polynomial Nimber} (h : p.natDegree < q.natDegree) : p < q

@[simp]

theorem Nimber.Lex.lt_X_pow_iff {p : Polynomial Nimber} {n : ℕ} : p < Polynomial.X ^ n ↔ p.degree < ↑n

@[simp]

theorem Nimber.Lex.coe_lt_X_pow_iff {p : Polynomial Nimber} {n : ℕ} : ↑p < ↑Polynomial.X ^ n ↔ p.degree < ↑n

@[simp]

theorem Nimber.Lex.X_pow_le_iff {p : Polynomial Nimber} {n : ℕ} : Polynomial.X ^ n ≤ p ↔ ↑n ≤ p.degree

@[simp]

theorem Nimber.Lex.X_pow_le_coe_iff {p : Polynomial Nimber} {n : ℕ} : ↑Polynomial.X ^ n ≤ ↑p ↔ ↑n ≤ p.degree

theorem Nimber.Lex.strictMono_X_pow : StrictMono fun (n : ℕ) => Polynomial.X ^ n

theorem Nimber.Lex.X_pow_le_X_pow_iff {m n : ℕ} : Polynomial.X ^ m ≤ Polynomial.X ^ n ↔ m ≤ n

theorem Nimber.Lex.X_pow_lt_X_pow_iff {m n : ℕ} : Polynomial.X ^ m < Polynomial.X ^ n ↔ m < n

@[simp]

theorem Nimber.Lex.coe_X_pow_le_coe_X_pow_iff {m n : ℕ} : ↑Polynomial.X ^ m ≤ ↑Polynomial.X ^ n ↔ m ≤ n

@[simp]

theorem Nimber.Lex.coe_X_pow_lt_coe_X_pow_iff {m n : ℕ} : ↑Polynomial.X ^ m < ↑Polynomial.X ^ n ↔ m < n

theorem Nimber.Lex.X_pow_add_lt {p q : Polynomial Nimber} (hm : p.Monic) (h : q < Polynomial.X ^ p.natDegree + p) : Polynomial.X ^ p.natDegree + q < p

theorem Nimber.Lex.X_pow_add_le {p q : Polynomial Nimber} (hm : p.Monic) (h : q ≤ Polynomial.X ^ p.natDegree + p) : Polynomial.X ^ p.natDegree + q ≤ p

theorem Nimber.Lex.mul_leadingCoeff_inv_lt {p : Polynomial Nimber} (h₀ : p ≠ 0) (h₁ : ¬p.Monic) : p * Polynomial.C p.leadingCoeff⁻¹ < p

theorem Nimber.Lex.mul_leadingCoeff_inv_le (p : Polynomial Nimber) : p * Polynomial.C p.leadingCoeff⁻¹ ≤ p

instance Nimber.Lex.instNoMaxOrderPolynomial : NoMaxOrder (Polynomial Nimber)

@[instance_reducible]

noncomputable instance Nimber.Lex.instSuccOrderPolynomial : SuccOrder (Polynomial Nimber)

Equations

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

theorem Nimber.Lex.coeff_succ (p : Polynomial Nimber) : ⇑(Order.succ p).coeff = Function.update (⇑p.coeff) 0 (Order.succ (p.coeff 0))

@[simp]

theorem Nimber.Lex.coeff_succ_zero (p : Polynomial Nimber) : (Order.succ p).coeff 0 = Order.succ (p.coeff 0)

@[simp]

theorem Nimber.Lex.coeff_succ_of_ne_zero (p : Polynomial Nimber) {k : ℕ} (h : k ≠ 0) : (Order.succ p).coeff k = p.coeff k

theorem Nimber.Lex.succ_eq_add_one_of_coeff_zero {p : Polynomial Nimber} (h : p.coeff 0 = 0) : Order.succ p = p + 1

Evaluating nimber polynomials as ordinals

noncomputable def Nimber.oeval (x : Nimber) (p : Polynomial Nimber) : Nimber

Evaluate a nimber polynomial using ordinal arithmetic.

TODO: once the Ordinal.CNF API is more developed, use it to redefine this.

Equations

• x.oeval p = Nimber.of (List.map (fun (k : ℕ) => Nimber.val x ^ k * Nimber.val (p.coeff k)) (List.range (p.natDegree + 1)).reverse).sum

@[simp]

theorem Nimber.oeval_zero (x : Nimber) : x.oeval 0 = 0

theorem Nimber.oeval_eq_of_natDegree_le {p : Polynomial Nimber} {n : ℕ} (h : p.natDegree + 1 ≤ n) (x : Nimber) : x.oeval p = of (List.map (fun (k : ℕ) => val x ^ k * val (p.coeff k)) (List.range n).reverse).sum

theorem Nimber.oeval_C_mul_X_pow_add {n : ℕ} {p : Polynomial Nimber} (hp : p.degree < ↑n) (x a : Nimber) : x.oeval (Polynomial.C a * Polynomial.X ^ n + p) = of (val x ^ n * val a + val (x.oeval p))

theorem Nimber.oeval_eq (x : Nimber) (p : Polynomial Nimber) : x.oeval p = of (val x ^ p.natDegree * val p.leadingCoeff + val (x.oeval p.eraseLead))

@[simp]

theorem Nimber.oeval_X_pow_mul (x : Nimber) (n : ℕ) (p : Polynomial Nimber) : x.oeval (Polynomial.X ^ n * p) = of (val x ^ n * val (x.oeval p))

@[simp]

theorem Nimber.oeval_mul_X_pow (x : Nimber) (n : ℕ) (p : Polynomial Nimber) : x.oeval (p * Polynomial.X ^ n) = of (val x ^ n * val (x.oeval p))

theorem Nimber.oeval_C_mul_X_pow (x a : Nimber) (n : ℕ) : x.oeval (Polynomial.C a * Polynomial.X ^ n) = of (val x ^ n * val a)

@[simp]

theorem Nimber.oeval_X_pow (x : Nimber) (n : ℕ) : x.oeval (Polynomial.X ^ n) = of (val x ^ n)

@[simp]

theorem Nimber.oeval_X (x : Nimber) : x.oeval Polynomial.X = x

@[simp]

theorem Nimber.oeval_C (x a : Nimber) : x.oeval (Polynomial.C a) = a

@[simp]

theorem Nimber.oeval_one (x : Nimber) : x.oeval 1 = 1

theorem Nimber.mul_coeff_le_oeval (x : Nimber) (p : Polynomial Nimber) (k : ℕ) : of (val x ^ k * val (p.coeff k)) ≤ x.oeval p

theorem Nimber.opow_natDegree_le_oeval (x : Nimber) {p : Polynomial Nimber} (hp : p ≠ 0) : of (val x ^ p.natDegree) ≤ x.oeval p

theorem Nimber.oeval_lt_pow {x : Nimber} {p : Polynomial Nimber} {n : ℕ} (hpk : ∀ (k : ℕ), p.coeff k < x) (hn : p.degree < ↑n) : x.oeval p < of (val x ^ n)

theorem Nimber.oeval_lt_pow_iff {x : Nimber} {p : Polynomial Nimber} {n : ℕ} (hpk : ∀ (k : ℕ), p.coeff k < x) : x.oeval p < of (val x ^ n) ↔ p.degree < ↑n

theorem Nimber.oeval_lt_opow_omega0 {x : Nimber} {p : Polynomial Nimber} (hpk : ∀ (k : ℕ), p.coeff k < x) : x.oeval p < of (val x ^ Ordinal.omega0)

theorem Nimber.oeval_lt_oeval {x : Nimber} {p q : Polynomial Nimber} (h : p < q) (hpk : ∀ (k : ℕ), p.coeff k < x) (hqk : ∀ (k : ℕ), q.coeff k < x) : x.oeval p < x.oeval q

theorem Nimber.oeval_le_oeval {x : Nimber} {p q : Polynomial Nimber} (h : p ≤ q) (hpk : ∀ (k : ℕ), p.coeff k < x) (hqk : ∀ (k : ℕ), q.coeff k < x) : x.oeval p ≤ x.oeval q

theorem Nimber.oeval_lt_oeval_iff {x : Nimber} {p q : Polynomial Nimber} (hpk : ∀ (k : ℕ), p.coeff k < x) (hqk : ∀ (k : ℕ), q.coeff k < x) : x.oeval p < x.oeval q ↔ p < q

theorem Nimber.oeval_le_oeval_iff {x : Nimber} {p q : Polynomial Nimber} (hpk : ∀ (k : ℕ), p.coeff k < x) (hqk : ∀ (k : ℕ), q.coeff k < x) : x.oeval p ≤ x.oeval q ↔ p ≤ q

theorem Nimber.oeval_inj {x : Nimber} {p q : Polynomial Nimber} (hpk : ∀ (k : ℕ), p.coeff k < x) (hqk : ∀ (k : ℕ), q.coeff k < x) : x.oeval p = x.oeval q ↔ p = q

theorem Nimber.oeval_eq_zero_iff {x : Nimber} {p : Polynomial Nimber} (hx : x ≠ 0) : x.oeval p = 0 ↔ p = 0

theorem Nimber.eq_oeval_of_lt_pow' {x y : Ordinal.{u_1}} {n : ℕ} (hx₀ : x ≠ 0) (h : y < x ^ n) : ∃ (p : Polynomial Nimber), p.degree < ↑n ∧ (∀ (k : ℕ), val (p.coeff k) < x) ∧ val ((of x).oeval p) = y

A version of eq_oeval_of_lt_pow stated in terms of Ordinal.

theorem Nimber.eq_oeval_of_lt_pow {x y : Nimber} {n : ℕ} (hx₀ : x ≠ 0) (h : y < of (val x ^ n)) : ∃ (p : Polynomial Nimber), p.degree < ↑n ∧ (∀ (k : ℕ), p.coeff k < x) ∧ x.oeval p = y

theorem Nimber.eq_oeval_of_lt_opow_omega0 {x y : Nimber} (h : y < of (val x ^ Ordinal.omega0)) : ∃ (p : Polynomial Nimber), (∀ (k : ℕ), p.coeff k < x) ∧ x.oeval p = y

theorem Nimber.eq_oeval_of_lt_oeval {x y : Nimber} {p : Polynomial Nimber} (hx₀ : x ≠ 0) (hpk : ∀ (k : ℕ), p.coeff k < x) (h : y < x.oeval p) : ∃ q < p, (∀ (k : ℕ), q.coeff k < x) ∧ x.oeval q = y

theorem Nimber.forall_lt_oeval_iff {x : Nimber} {P : Nimber → Prop} {p : Polynomial Nimber} (hpk : ∀ (k : ℕ), p.coeff k < x) : (∀ y < x.oeval p, P y) ↔ ∀ q < p, (∀ (k : ℕ), q.coeff k < x) → P (x.oeval q)

Least irreducible polynomial

noncomputable def Nimber.leastNoRoots (x : Nimber) : WithTop (Polynomial Nimber)

Returns the lexicographically earliest non-constant polynomial, all of whose coefficients are less than x, without any roots less than x. If none exists, returns ⊤.

This function takes values on WithTop (Nimber[X]), which is a well-ordered complete lattice (the order on Nimber[X] is the lexicographic order).

Equations

• x.leastNoRoots = sInf (WithTop.some '' {p : Polynomial Nimber | 0 < p.degree ∧ (∀ (k : ℕ), p.coeff k < x) ∧ ∀ r < x, Polynomial.eval r p ≠ 0})

theorem Nimber.degree_leastNoRoots_pos {x : Nimber} (ht : x.leastNoRoots ≠ ⊤) : 0 < (x.leastNoRoots.untop ht).degree

theorem Nimber.natDegree_leastNoRoots_pos {x : Nimber} (ht : x.leastNoRoots ≠ ⊤) : 0 < (x.leastNoRoots.untop ht).natDegree

theorem Nimber.one_le_degree_leastNoRoots_pos {x : Nimber} (ht : x.leastNoRoots ≠ ⊤) : 1 ≤ (x.leastNoRoots.untop ht).degree

theorem Nimber.one_le_natDegree_leastNoRoots {x : Nimber} (ht : x.leastNoRoots ≠ ⊤) : 1 ≤ (x.leastNoRoots.untop ht).natDegree

theorem Nimber.coeff_leastNoRoots_lt {x : Nimber} (ht : x.leastNoRoots ≠ ⊤) (k : ℕ) : (x.leastNoRoots.untop ht).coeff k < x

theorem Nimber.not_isRoot_leastNoRoots_of_lt {x r : Nimber} (ht : x.leastNoRoots ≠ ⊤) (hr : r < x) : ¬(x.leastNoRoots.untop ht).IsRoot r

@[simp]

theorem Nimber.leastNoRoots_zero : leastNoRoots 0 = ⊤

@[simp]

theorem Nimber.leastNoRoots_one : leastNoRoots 1 = ⊤

theorem Nimber.leastNoRoots_of_le_one {x : Nimber} (h : x ≤ 1) : x.leastNoRoots = ⊤

@[simp]

theorem Nimber.coeff_leastNoRoots_zero_ne {x : Nimber} (ht : x.leastNoRoots ≠ ⊤) : (x.leastNoRoots.untop ht).coeff 0 ≠ 0

@[simp]

theorem Nimber.leastNoRoots_ne_zero (x : Nimber) : x.leastNoRoots ≠ 0

@[simp]

theorem Nimber.leastNoRoots_ne_zero' {x : Nimber} (ht : x.leastNoRoots ≠ ⊤) : x.leastNoRoots.untop ht ≠ 0

theorem Nimber.leastNoRoots_ne_X_pow' (x : Nimber) (ht : x.leastNoRoots ≠ ⊤) (n : ℕ) : x.leastNoRoots.untop ht ≠ Polynomial.X ^ n

theorem Nimber.leastNoRoots_ne_X_pow (x : Nimber) (n : ℕ) : x.leastNoRoots ≠ ↑(Polynomial.X ^ n)

theorem Nimber.X_pow_lt_leastNoRoots_of_le_degree {x : Nimber} {n : ℕ} (ht : x.leastNoRoots ≠ ⊤) (h : ↑n ≤ (x.leastNoRoots.untop ht).degree) : ↑(Polynomial.X ^ n) < x.leastNoRoots

theorem Nimber.leastNoRoots_le_of_not_isRoot {x : Nimber} {p : Polynomial Nimber} (hp₀ : 0 < p.degree) (hpk : ∀ (k : ℕ), p.coeff k < x) (hr : ∀ r < x, ¬p.IsRoot r) : x.leastNoRoots ≤ ↑p

theorem Nimber.exists_root_of_lt_leastNoRoots {x : Nimber} {p : Polynomial Nimber} (hp₀ : p.degree ≠ 0) (hpk : ∀ (k : ℕ), p.coeff k < x) (hpn : ↑p < x.leastNoRoots) : ∃ r < x, p.IsRoot r

theorem Nimber.le_leastNoRoots_of_exists_isRoot {x : Nimber} {p : Polynomial Nimber} (hp : ∀ c < p, 0 < c.degree → (∀ (k : ℕ), c.coeff k < x) → ∃ r < x, c.IsRoot r) : ↑p ≤ x.leastNoRoots

theorem Nimber.IsField.exists_root_subfield {x : Nimber} (h : x.IsField) {p : Polynomial ↥h.toSubfield} (hp₀ : p.degree ≠ 0) (hpn : ↑(Polynomial.map h.toSubfield.subtype p) < x.leastNoRoots) : ∃ (r : ↥h.toSubfield), p.IsRoot r

theorem Nimber.IsField.splits_subfield {x : Nimber} (h : x.IsField) {p : Polynomial ↥h.toSubfield} (hpn : ↑(Polynomial.map h.toSubfield.subtype p) < x.leastNoRoots) : p.Splits

theorem Nimber.IsField.roots_eq_map {x : Nimber} (h : x.IsField) {p : Polynomial Nimber} (hpn : ↑p < x.leastNoRoots) (hpk : ∀ (k : ℕ), p.coeff k < x) : p.roots = Multiset.map (⇑h.toSubfield.subtype) (h.embed p hpk).roots

theorem Nimber.IsField.root_lt {x r : Nimber} (h : x.IsField) {p : Polynomial Nimber} (hpn : ↑p < x.leastNoRoots) (hpk : ∀ (k : ℕ), p.coeff k < x) (hr : r ∈ p.roots) : r < x

theorem Nimber.IsField.eq_prod_roots_of_lt_leastNoRoots {x : Nimber} (h : x.IsField) {p : Polynomial Nimber} (hpn : ↑p < x.leastNoRoots) (hpk : ∀ (k : ℕ), p.coeff k < x) : p = Polynomial.C p.leadingCoeff * (Multiset.map (fun (a : Nimber) => Polynomial.X - Polynomial.C a) p.roots).prod

theorem Nimber.IsRing.leastNoRoots_eq_of_not_isField {x : Nimber} (h : x.IsRing) (h' : ¬x.IsField) : x.leastNoRoots = ↑(Polynomial.C x⁻¹ * Polynomial.X + 1)

theorem Nimber.IsField.X_sq_lt_leastNoRoots {x : Nimber} (h : x.IsField) : ↑(Polynomial.X ^ 2) < x.leastNoRoots

theorem Nimber.IsRing.toIsField_of_X_sq_lt_leastNoRoots {x : Nimber} (h : x.IsRing) (h' : ↑(Polynomial.X ^ 2) ≤ x.leastNoRoots) : x.IsField

theorem Nimber.IsField.monic_leastNoRoots {x : Nimber} (h : x.IsField) (ht : x.leastNoRoots ≠ ⊤) : (x.leastNoRoots.untop ht).Monic

theorem Nimber.IsField.irreducible_embed_leastNoRoots {x : Nimber} (h : x.IsField) (ht : x.leastNoRoots ≠ ⊤) : Irreducible (h.embed (x.leastNoRoots.untop ht) ⋯)

theorem Polynomial.exists_gt_of_forall_coeff_gt {s : Set Nimber} {p : Polynomial Nimber} (h : ∀ (k : ℕ), ∃ a ∈ s, p.coeff k < a) : ∃ a ∈ s, ∀ (k : ℕ), p.coeff k < a

theorem Nimber.le_leastNoRoots_sSup {s : Set Nimber} {p : WithTop (Polynomial Nimber)} (H : ∀ x ∈ s, p ≤ x.leastNoRoots) : p ≤ (sSup s).leastNoRoots

theorem Nimber.le_leastNoRoots_iSup {ι : Sort u_1} {f : ι → Nimber} {p : WithTop (Polynomial Nimber)} (H : ∀ (i : ι), p ≤ (f i).leastNoRoots) : p ≤ (⨆ (i : ι), f i).leastNoRoots