Documentation

Mathlib.Data.Polynomial.Degree.Lemmas

Theory of degrees of polynomials #

Some of the main results include

theorem Polynomial.degree_pos_of_root {R : Type u} {a : R} [Semiring R] {p : Polynomial R} (hp : p 0) (h : Polynomial.IsRoot p a) :
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) :
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) :

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

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

theorem Polynomial.coeff_pow_eq_ite_of_natDegree_le_of_le {R : Type u} {m : } {n : } [Semiring R] {p : Polynomial R} {o : } (pn : Polynomial.natDegree p n) (mno : m * n o) :
Polynomial.coeff (p ^ m) o = if o = m * n then Polynomial.coeff p n ^ m else 0
theorem Polynomial.degree_sum_eq_of_disjoint {R : Type u} {S : Type v} [Semiring R] (f : SPolynomial R) (s : Finset S) (h : Set.Pairwise {i : S | i s f i 0} (Ne on Polynomial.degree f)) :
theorem Polynomial.natDegree_sum_eq_of_disjoint {R : Type u} {S : Type v} [Semiring R] (f : SPolynomial R) (s : Finset S) (h : Set.Pairwise {i : S | i s f i 0} (Ne on Polynomial.natDegree f)) :
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 : Polynomial.eval₂ f z p = 0) (inj : ∀ (x : R), f x = 0x = 0) :
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 : Polynomial.eval₂ f z p = 0) (inj : ∀ (x : R), f x = 0x = 0) :
theorem Polynomial.degree_mul_C {R : Type u} [Semiring R] [NoZeroDivisors R] {p : Polynomial R} {a : R} (a0 : a 0) :
Polynomial.degree (p * Polynomial.C a) = Polynomial.degree p
theorem Polynomial.degree_C_mul {R : Type u} [Semiring R] [NoZeroDivisors R] {p : Polynomial R} {a : R} (a0 : a 0) :
Polynomial.degree (Polynomial.C a * p) = Polynomial.degree p
theorem Polynomial.natDegree_mul_C {R : Type u} [Semiring R] [NoZeroDivisors R] {p : Polynomial R} {a : R} (a0 : a 0) :
theorem Polynomial.natDegree_C_mul {R : Type u} [Semiring R] [NoZeroDivisors R] {p : Polynomial R} {a : R} (a0 : a 0) :
@[simp]
theorem Polynomial.nextCoeff_C_mul_X_add_C {R : Type u} [Semiring R] {a : R} (ha : a 0) (c : R) :
Polynomial.nextCoeff (Polynomial.C a * Polynomial.X + Polynomial.C c) = c
theorem Polynomial.natDegree_eq_one {R : Type u} [Semiring R] {p : Polynomial R} :
Polynomial.natDegree p = 1 ∃ (a : R), a 0 ∃ (b : R), Polynomial.C a * Polynomial.X + Polynomial.C b = p

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

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