Theory of degrees of polynomials

Some of the main results include

• natDegree_comp_le : The degree of the composition is at most the product of degrees

theorem Polynomial.natDegree_comp_le {R : Type u} [Semiring R] {p q : Polynomial R} : (p.comp q).natDegree ≤ p.natDegree * q.natDegree

theorem Polynomial.natDegree_comp_eq_of_mul_ne_zero {R : Type u} [Semiring R] {p q : Polynomial R} (h : p.leadingCoeff * q.leadingCoeff ^ p.natDegree ≠ 0) : (p.comp q).natDegree = p.natDegree * q.natDegree

theorem Polynomial.degree_pos_of_root {R : Type u} {a : R} [Semiring R] {p : Polynomial R} (hp : p ≠ 0) (h : p.IsRoot a) : 0 < p.degree

theorem Polynomial.natDegree_le_iff_coeff_eq_zero {R : Type u} {n : ℕ} [Semiring R] {p : Polynomial R} : p.natDegree ≤ n ↔ ∀ (N : ℕ), n < N → p.coeff N = 0

theorem Polynomial.natDegree_add_le_iff_left {R : Type u} [Semiring R] {n : ℕ} (p q : Polynomial R) (qn : q.natDegree ≤ n) : (p + q).natDegree ≤ n ↔ p.natDegree ≤ n

theorem Polynomial.natDegree_add_le_iff_right {R : Type u} [Semiring R] {n : ℕ} (p q : Polynomial R) (pn : p.natDegree ≤ n) : (p + q).natDegree ≤ n ↔ q.natDegree ≤ n

theorem Polynomial.natDegree_C_mul_le {R : Type u} [Semiring R] (a : R) (f : Polynomial R) : (C a * f).natDegree ≤ f.natDegree

theorem Polynomial.natDegree_mul_C_le {R : Type u} [Semiring R] (f : Polynomial R) (a : R) : (f * C a).natDegree ≤ f.natDegree

theorem Polynomial.eq_natDegree_of_le_mem_support {R : Type u} {n : ℕ} [Semiring R] {p : Polynomial R} (pn : p.natDegree ≤ n) (ns : n ∈ p.support) : p.natDegree = n

theorem Polynomial.natDegree_C_mul_eq_of_mul_eq_one {R : Type u} {a : R} [Semiring R] {p : Polynomial R} {ai : R} (au : ai * a = 1) : (C a * p).natDegree = p.natDegree

theorem Polynomial.natDegree_mul_C_eq_of_mul_eq_one {R : Type u} {a : R} [Semiring R] {p : Polynomial R} {ai : R} (au : a * ai = 1) : (p * C a).natDegree = p.natDegree

theorem Polynomial.natDegree_mul_C_eq_of_mul_ne_zero {R : Type u} {a : R} [Semiring R] {p : Polynomial R} (h : p.leadingCoeff * a ≠ 0) : (p * C a).natDegree = p.natDegree

Although not explicitly stated, the assumptions of lemma natDegree_mul_C_eq_of_mul_ne_zero force the polynomial p to be non-zero, via p.leadingCoeff ≠ 0.

theorem Polynomial.natDegree_C_mul_of_mul_ne_zero {R : Type u} {a : R} [Semiring R] {p : Polynomial R} (h : a * p.leadingCoeff ≠ 0) : (C a * p).natDegree = p.natDegree

Although not explicitly stated, the assumptions of lemma natDegree_C_mul_of_mul_ne_zero force the polynomial p to be non-zero, via p.leadingCoeff ≠ 0.

theorem Polynomial.degree_C_mul_of_mul_ne_zero {R : Type u} {a : R} [Semiring R] {p : Polynomial R} (h : a * p.leadingCoeff ≠ 0) : (C a * p).degree = p.degree

theorem Polynomial.natDegree_add_coeff_mul {R : Type u} [Semiring R] (f g : Polynomial R) : (f * g).coeff (f.natDegree + g.natDegree) = f.coeff f.natDegree * g.coeff g.natDegree

theorem Polynomial.natDegree_lt_coeff_mul {R : Type u} {m n : ℕ} [Semiring R] {p q : Polynomial R} (h : p.natDegree + q.natDegree < m + n) : (p * q).coeff (m + n) = 0

theorem Polynomial.coeff_pow_of_natDegree_le {R : Type u} {m n : ℕ} [Semiring R] {p : Polynomial R} (pn : p.natDegree ≤ n) : (p ^ m).coeff (m * n) = p.coeff n ^ m

theorem Polynomial.coeff_pow_eq_ite_of_natDegree_le_of_le {R : Type u} {m n : ℕ} [Semiring R] {p : Polynomial R} {o : ℕ} (pn : p.natDegree ≤ n) (mno : m * n ≤ o) : (p ^ m).coeff o = if o = m * n then p.coeff n ^ m else 0

theorem Polynomial.coeff_add_eq_left_of_lt {R : Type u} {n : ℕ} [Semiring R] {p q : Polynomial R} (qn : q.natDegree < n) : (p + q).coeff n = p.coeff n

theorem Polynomial.coeff_add_eq_right_of_lt {R : Type u} {n : ℕ} [Semiring R] {p q : Polynomial R} (pn : p.natDegree < n) : (p + q).coeff n = q.coeff n

theorem Polynomial.degree_sum_eq_of_disjoint {R : Type u} {S : Type v} [Semiring R] (f : S → Polynomial R) (s : Finset S) (h : {i : S | i ∈ s ∧ f i ≠ 0}.Pairwise (Function.onFun Ne (degree ∘ f))) : (s.sum f).degree = s.sup fun (i : S) => (f i).degree

theorem Polynomial.natDegree_sum_eq_of_disjoint {R : Type u} {S : Type v} [Semiring R] (f : S → Polynomial R) (s : Finset S) (h : {i : S | i ∈ s ∧ f i ≠ 0}.Pairwise (Function.onFun Ne (natDegree ∘ f))) : (s.sum f).natDegree = s.sup fun (i : S) => (f i).natDegree

theorem Polynomial.natDegree_pos_of_eval₂_root {R : Type u} {S : Type v} [Semiring R] [Semiring S] {p : Polynomial R} (hp : p ≠ 0) (f : R →+* S) {z : S} (hz : eval₂ f z p = 0) (inj : ∀ (x : R), f x = 0 → x = 0) : 0 < p.natDegree

theorem Polynomial.degree_pos_of_eval₂_root {R : Type u} {S : Type v} [Semiring R] [Semiring S] {p : Polynomial R} (hp : p ≠ 0) (f : R →+* S) {z : S} (hz : eval₂ f z p = 0) (inj : ∀ (x : R), f x = 0 → x = 0) : 0 < p.degree

@[simp]

theorem Polynomial.coe_lt_degree {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} : ↑n < p.degree ↔ n < p.natDegree

@[simp]

theorem Polynomial.degree_map_eq_iff {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} {p : Polynomial R} : (map f p).degree = p.degree ↔ f p.leadingCoeff ≠ 0 ∨ p = 0

@[simp]

theorem Polynomial.natDegree_map_eq_iff {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} {p : Polynomial R} : (map f p).natDegree = p.natDegree ↔ f p.leadingCoeff ≠ 0 ∨ p.natDegree = 0

theorem Polynomial.degree_map_eq_of_isUnit_leadingCoeff {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] [Nontrivial S] (f : R →+* S) (hp : IsUnit p.leadingCoeff) : (map f p).degree = p.degree

theorem Polynomial.natDegree_map_eq_of_isUnit_leadingCoeff {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] [Nontrivial S] (f : R →+* S) (hp : IsUnit p.leadingCoeff) : (map f p).natDegree = p.natDegree

theorem Polynomial.leadingCoeff_map_eq_of_isUnit_leadingCoeff {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] [Nontrivial S] (f : R →+* S) (hp : IsUnit p.leadingCoeff) : (map f p).leadingCoeff = f p.leadingCoeff

theorem Polynomial.nextCoeff_map_eq_of_isUnit_leadingCoeff {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] [Nontrivial S] (f : R →+* S) (hp : IsUnit p.leadingCoeff) : (map f p).nextCoeff = f p.nextCoeff

theorem Polynomial.degree_map_eq_of_injective {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} (hf : Function.Injective ⇑f) (p : Polynomial R) : (map f p).degree = p.degree

theorem Polynomial.natDegree_map_eq_of_injective {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} (hf : Function.Injective ⇑f) (p : Polynomial R) : (map f p).natDegree = p.natDegree

theorem Polynomial.leadingCoeff_map_of_injective {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} (hf : Function.Injective ⇑f) (p : Polynomial R) : (map f p).leadingCoeff = f p.leadingCoeff

theorem Polynomial.nextCoeff_map {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} (hf : Function.Injective ⇑f) (p : Polynomial R) : (map f p).nextCoeff = f p.nextCoeff

theorem Polynomial.natDegree_pos_of_nextCoeff_ne_zero {R : Type u} [Semiring R] {p : Polynomial R} (h : p.nextCoeff ≠ 0) : 0 < p.natDegree

theorem Polynomial.natDegree_sub {R : Type u} [Ring R] {p q : Polynomial R} : (p - q).natDegree = (q - p).natDegree

theorem Polynomial.natDegree_sub_le_iff_left {R : Type u} {n : ℕ} [Ring R] {p q : Polynomial R} (qn : q.natDegree ≤ n) : (p - q).natDegree ≤ n ↔ p.natDegree ≤ n

theorem Polynomial.natDegree_sub_le_iff_right {R : Type u} {n : ℕ} [Ring R] {p q : Polynomial R} (pn : p.natDegree ≤ n) : (p - q).natDegree ≤ n ↔ q.natDegree ≤ n

theorem Polynomial.coeff_sub_eq_left_of_lt {R : Type u} {n : ℕ} [Ring R] {p q : Polynomial R} (dg : q.natDegree < n) : (p - q).coeff n = p.coeff n

theorem Polynomial.coeff_sub_eq_neg_right_of_lt {R : Type u} {n : ℕ} [Ring R] {p q : Polynomial R} (df : p.natDegree < n) : (p - q).coeff n = -q.coeff n

@[simp]

theorem Polynomial.nextCoeff_C_mul_X_add_C {R : Type u} [Semiring R] {a : R} (ha : a ≠ 0) (c : R) : (C a * X + C c).nextCoeff = c

theorem Polynomial.natDegree_eq_one {R : Type u} [Semiring R] {p : Polynomial R} : p.natDegree = 1 ↔ ∃ (a : R), a ≠ 0 ∧ ∃ (b : R), C a * X + C b = p

theorem Polynomial.subsingleton_isRoot_of_natDegree_eq_one {R : Type u} [Semiring R] {p : Polynomial R} [IsLeftCancelMulZero R] (h : p.natDegree = 1) : {x : R | p.IsRoot x}.Subsingleton

theorem Polynomial.degree_mul_C {R : Type u} [Semiring R] {p : Polynomial R} {a : R} [NoZeroDivisors R] (a0 : a ≠ 0) : (p * C a).degree = p.degree

theorem Polynomial.degree_C_mul {R : Type u} [Semiring R] {p : Polynomial R} {a : R} [NoZeroDivisors R] (a0 : a ≠ 0) : (C a * p).degree = p.degree

theorem Polynomial.natDegree_mul_C {R : Type u} [Semiring R] {p : Polynomial R} {a : R} [NoZeroDivisors R] (a0 : a ≠ 0) : (p * C a).natDegree = p.natDegree

theorem Polynomial.natDegree_C_mul {R : Type u} [Semiring R] {p : Polynomial R} {a : R} [NoZeroDivisors R] (a0 : a ≠ 0) : (C a * p).natDegree = p.natDegree

theorem Polynomial.natDegree_comp {R : Type u} [Semiring R] {p q : Polynomial R} [NoZeroDivisors R] : (p.comp q).natDegree = p.natDegree * q.natDegree

@[simp]

theorem Polynomial.natDegree_iterate_comp {R : Type u} [Semiring R] {p q : Polynomial R} [NoZeroDivisors R] (k : ℕ) : (p.comp^[k] q).natDegree = p.natDegree ^ k * q.natDegree

theorem Polynomial.leadingCoeff_comp {R : Type u} [Semiring R] {p q : Polynomial R} [NoZeroDivisors R] (hq : q.natDegree ≠ 0) : (p.comp q).leadingCoeff = p.leadingCoeff * q.leadingCoeff ^ p.natDegree

@[simp]

theorem Polynomial.nextCoeff_C_mul {R : Type u} [Semiring R] {p : Polynomial R} {a : R} [NoZeroDivisors R] : (C a * p).nextCoeff = a * p.nextCoeff

@[simp]

theorem Polynomial.nextCoeff_mul_C {R : Type u} [Semiring R] {p : Polynomial R} {a : R} [NoZeroDivisors R] : (p * C a).nextCoeff = p.nextCoeff * a

@[simp]

theorem Polynomial.comp_neg_X_leadingCoeff_eq {R : Type u} [Ring R] (p : Polynomial R) : (p.comp (-X)).leadingCoeff = (-1) ^ p.natDegree * p.leadingCoeff

@[simp]

theorem Polynomial.comp_neg_X_eq_zero_iff {R : Type u} [Ring R] {p : Polynomial R} : p.comp (-X) = 0 ↔ p = 0

theorem Polynomial.comp_eq_zero_iff {R : Type u} [Semiring R] [NoZeroDivisors R] {p q : Polynomial R} : p.comp q = 0 ↔ p = 0 ∨ eval (q.coeff 0) p = 0 ∧ q = C (q.coeff 0)

theorem Polynomial.degree_comp {R : Type u} [Semiring R] [NoZeroDivisors R] {p q : Polynomial R} (hq : 0 < q.degree) : (p.comp q).degree = p.degree * q.degree

@[simp]

theorem Polynomial.degree_comp_neg_X {R : Type u} [Ring R] {p : Polynomial R} : (p.comp (-X)).degree = p.degree

Useful lemmas for the "monicization" of a nonzero polynomial p.

@[simp]

theorem Polynomial.irreducible_mul_leadingCoeff_inv {K : Type u_1} [DivisionRing K] {p : Polynomial K} : Irreducible (p * C p.leadingCoeff⁻¹) ↔ Irreducible p

theorem Polynomial.dvd_mul_leadingCoeff_inv {K : Type u_1} [DivisionRing K] {p q : Polynomial K} (hp0 : p ≠ 0) : q ∣ p * C p.leadingCoeff⁻¹ ↔ q ∣ p

theorem Polynomial.monic_mul_leadingCoeff_inv {K : Type u_1} [DivisionRing K] {p : Polynomial K} (h : p ≠ 0) : (p * C p.leadingCoeff⁻¹).Monic

theorem Polynomial.degree_leadingCoeff_inv {K : Type u_1} [DivisionRing K] {p : Polynomial K} (hp0 : p ≠ 0) : (C p.leadingCoeff⁻¹).degree = 0

theorem Polynomial.degree_mul_leadingCoeff_inv {K : Type u_1} [DivisionRing K] (p : Polynomial K) {q : Polynomial K} (h : q ≠ 0) : (p * C q.leadingCoeff⁻¹).degree = p.degree

theorem Polynomial.natDegree_mul_leadingCoeff_inv {K : Type u_1} [DivisionRing K] (p : Polynomial K) {q : Polynomial K} (h : q ≠ 0) : (p * C q.leadingCoeff⁻¹).natDegree = p.natDegree

theorem Polynomial.degree_mul_leadingCoeff_self_inv {K : Type u_1} [DivisionRing K] (p : Polynomial K) : (p * C p.leadingCoeff⁻¹).degree = p.degree

theorem Polynomial.natDegree_mul_leadingCoeff_self_inv {K : Type u_1} [DivisionRing K] (p : Polynomial K) : (p * C p.leadingCoeff⁻¹).natDegree = p.natDegree

@[simp]

theorem Polynomial.degree_add_degree_leadingCoeff_inv {K : Type u_1} [DivisionRing K] (p : Polynomial K) : p.degree + (C p.leadingCoeff⁻¹).degree = p.degree