Monic polynomials of given degree

This file defines the predicate Polynomial.IsMonicOfDegree p n that states that the polynomial p is monic and has degree n (i.e., p.natDegree = n.)

We also provide some basic API.

structure Polynomial.IsMonicOfDegree {R : Type u_1} [Semiring R] (p : Polynomial R) (n : ℕ) : Prop

This says that p has natDegree n and is monic.

• natDegree_eq : p.natDegree = n
• monic : p.Monic

theorem Polynomial.isMonicOfDegree_iff' {R : Type u_1} [Semiring R] (p : Polynomial R) (n : ℕ) : p.IsMonicOfDegree n ↔ p.natDegree = n ∧ p.Monic

@[simp]

theorem Polynomial.isMonicOfDegree_zero_iff {R : Type u_1} [Semiring R] {p : Polynomial R} : p.IsMonicOfDegree 0 ↔ p = 1

theorem Polynomial.IsMonicOfDegree.leadingCoeff_eq {R : Type u_1} [Semiring R] {p : Polynomial R} {n : ℕ} (hp : p.IsMonicOfDegree n) : p.leadingCoeff = 1

@[simp]

theorem Polynomial.isMonicOfDegree_iff_of_subsingleton {R : Type u_1} [Semiring R] [Subsingleton R] {p : Polynomial R} {n : ℕ} : p.IsMonicOfDegree n ↔ n = 0

theorem Polynomial.isMonicOfDegree_iff {R : Type u_1} [Semiring R] [Nontrivial R] (p : Polynomial R) (n : ℕ) : p.IsMonicOfDegree n ↔ p.natDegree ≤ n ∧ p.coeff n = 1

theorem Polynomial.IsMonicOfDegree.exists_natDegree_lt {R : Type u_1} [Semiring R] {p : Polynomial R} {n : ℕ} (hn : n ≠ 0) (hp : p.IsMonicOfDegree n) : ∃ (q : Polynomial R), p = X ^ n + q ∧ q.natDegree < n

theorem Polynomial.IsMonicOfDegree.mul {R : Type u_1} [Semiring R] {p q : Polynomial R} {m n : ℕ} (hp : p.IsMonicOfDegree m) (hq : q.IsMonicOfDegree n) : (p * q).IsMonicOfDegree (m + n)

theorem Polynomial.IsMonicOfDegree.pow {R : Type u_1} [Semiring R] {p : Polynomial R} {m : ℕ} (hp : p.IsMonicOfDegree m) (n : ℕ) : (p ^ n).IsMonicOfDegree (m * n)

theorem Polynomial.IsMonicOfDegree.coeff_eq {R : Type u_1} [Semiring R] {p q : Polynomial R} {n : ℕ} (hp : p.IsMonicOfDegree n) (hq : q.IsMonicOfDegree n) {m : ℕ} (hm : n ≤ m) : p.coeff m = q.coeff m

theorem Polynomial.IsMonicOfDegree.of_mul_left {R : Type u_1} [Semiring R] {p q : Polynomial R} {m n : ℕ} (hp : p.IsMonicOfDegree m) (hpq : (p * q).IsMonicOfDegree (m + n)) : q.IsMonicOfDegree n

theorem Polynomial.IsMonicOfDegree.of_mul_right {R : Type u_1} [Semiring R] {p q : Polynomial R} {m n : ℕ} (hq : q.IsMonicOfDegree n) (hpq : (p * q).IsMonicOfDegree (m + n)) : p.IsMonicOfDegree m

theorem Polynomial.IsMonicOfDegree.add_right {R : Type u_1} [Semiring R] {p q : Polynomial R} {n : ℕ} (hp : p.IsMonicOfDegree n) (hq : q.natDegree < n) : (p + q).IsMonicOfDegree n

theorem Polynomial.IsMonicOfDegree.add_left {R : Type u_1} [Semiring R] {p q : Polynomial R} {n : ℕ} (hp : p.natDegree < n) (hq : q.IsMonicOfDegree n) : (p + q).IsMonicOfDegree n

theorem Polynomial.IsMonicOfDegree.comp {R : Type u_1} [Semiring R] {p q : Polynomial R} {m n : ℕ} (hn : n ≠ 0) (hp : p.IsMonicOfDegree m) (hq : q.IsMonicOfDegree n) : (p.comp q).IsMonicOfDegree (m * n)

theorem Polynomial.IsMonicOfDegree.ne_zero {R : Type u_1} [Semiring R] [Nontrivial R] {p : Polynomial R} {n : ℕ} (h : p.IsMonicOfDegree n) : p ≠ 0

theorem Polynomial.isMonicOfDegree_X (R : Type u_1) [Semiring R] [Nontrivial R] : X.IsMonicOfDegree 1

theorem Polynomial.isMonicOfDegree_X_pow (R : Type u_1) [Semiring R] [Nontrivial R] (n : ℕ) : (X ^ n).IsMonicOfDegree n

theorem Polynomial.isMonicOfDegree_monomial_one {R : Type u_1} [Semiring R] [Nontrivial R] (n : ℕ) : ((monomial n) 1).IsMonicOfDegree n

theorem Polynomial.isMonicOfDegree_X_add_one {R : Type u_1} [Semiring R] [Nontrivial R] (r : R) : (X + C r).IsMonicOfDegree 1

theorem Polynomial.isMonicOfDegree_one_iff {R : Type u_1} [Semiring R] [Nontrivial R] {f : Polynomial R} : f.IsMonicOfDegree 1 ↔ ∃ (r : R), f = X + C r

theorem Polynomial.isMonicOfDegree_add_add_two {R : Type u_1} [Semiring R] [Nontrivial R] (a b : R) : (X ^ 2 + C a * X + C b).IsMonicOfDegree 2

theorem Polynomial.isMonicOfDegree_two_iff {R : Type u_1} [Semiring R] [Nontrivial R] {f : Polynomial R} : f.IsMonicOfDegree 2 ↔ ∃ (a : R) (b : R), f = X ^ 2 + C a * X + C b

theorem Polynomial.IsMonicOfDegree.natDegree_sub_X_pow {R : Type u_1} [Ring R] {p : Polynomial R} {n : ℕ} (hn : n ≠ 0) (hp : p.IsMonicOfDegree n) : (p - X ^ n).natDegree < n

theorem Polynomial.IsMonicOfDegree.natDegree_sub_lt {R : Type u_1} [Ring R] {p q : Polynomial R} {n : ℕ} (hn : n ≠ 0) (hp : p.IsMonicOfDegree n) (hq : q.IsMonicOfDegree n) : (p - q).natDegree < n

theorem Polynomial.IsMonicOfDegree.sub {R : Type u_1} [Ring R] {p q : Polynomial R} {n : ℕ} (hp : p.IsMonicOfDegree n) (hq : q.natDegree < n) : (p - q).IsMonicOfDegree n

theorem Polynomial.isMonicOfDegree_X_sub_one {R : Type u_1} [Ring R] [Nontrivial R] (r : R) : (X - C r).IsMonicOfDegree 1

theorem Polynomial.isMonicOfDegree_sub_add_two {R : Type u_1} [Ring R] [Nontrivial R] (a b : R) : (X ^ 2 - C a * X + C b).IsMonicOfDegree 2

theorem Polynomial.isMonicOfDegree_two_iff' {R : Type u_1} [Ring R] [Nontrivial R] {f : Polynomial R} : f.IsMonicOfDegree 2 ↔ ∃ (a : R) (b : R), f = X ^ 2 - C a * X + C b

A version of Polynomial.isMonicOfDegree_two_iff with negated middle coefficient.

theorem Polynomial.IsMonicOfDegree.of_dvd_add {R : Type u_1} [CommRing R] {a b r : Polynomial R} {m n : ℕ} (hmn : n ≤ m) (ha : a.IsMonicOfDegree m) (hb : b.IsMonicOfDegree n) (hr : r.natDegree < m) (h : b ∣ a + r) : ∃ (q : Polynomial R), q.IsMonicOfDegree (m - n) ∧ a = q * b - r

theorem Polynomial.IsMonicOfDegree.of_dvd_sub {R : Type u_1} [CommRing R] {a b r : Polynomial R} {m n : ℕ} (hmn : n ≤ m) (ha : a.IsMonicOfDegree m) (hb : b.IsMonicOfDegree n) (hr : r.natDegree < m) (h : b ∣ a - r) : ∃ (q : Polynomial R), q.IsMonicOfDegree (m - n) ∧ a = q * b + r

theorem Polynomial.IsMonicOfDegree.aeval_add {R : Type u_1} [CommRing R] {p : Polynomial R} {n : ℕ} (hp : p.IsMonicOfDegree n) (r : R) : ((aeval (X + C r)) p).IsMonicOfDegree n

theorem Polynomial.IsMonicOfDegree.aeval_sub {R : Type u_1} [CommRing R] {p : Polynomial R} {n : ℕ} (hp : p.IsMonicOfDegree n) (r : R) : ((aeval (X - C r)) p).IsMonicOfDegree n