# Theory of univariate polynomials #

This file starts looking like the ring theory of $R[X]$

source
theorem Polynomial.rootMultiplicity_sub_one_le_derivative_rootMultiplicity_of_ne_zero {R : Type u} [CommRing R] (p : Polynomial R) (t : R) (hnezero : derivative p ≠ 0) :
rootMultiplicity t p - 1 ≤ rootMultiplicity t (derivative p)
source
theorem Polynomial.derivative_rootMultiplicity_of_root_of_mem_nonZeroDivisors {R : Type u} [CommRing R] {p : Polynomial R} {t : R} (hpt : p.IsRoot t) (hnzd : ↑(rootMultiplicity t p) ∈ nonZeroDivisors R) :
rootMultiplicity t (derivative p) = rootMultiplicity t p - 1
source
theorem Polynomial.isRoot_iterate_derivative_of_lt_rootMultiplicity {R : Type u} [CommRing R] {p : Polynomial R} {t : R} {n : ℕ} (hn : n < rootMultiplicity t p) :
((⇑derivative)^[n] p).IsRoot t
source
theorem Polynomial.eval_iterate_derivative_rootMultiplicity {R : Type u} [CommRing R] {p : Polynomial R} {t : R} :
eval t ((⇑derivative)^[rootMultiplicity t p] p) = (rootMultiplicity t p).factorial • eval t (p /ₘ (X - C t) ^ rootMultiplicity t p)
source
theorem Polynomial.lt_rootMultiplicity_of_isRoot_iterate_derivative_of_mem_nonZeroDivisors {R : Type u} [CommRing R] {p : Polynomial R} {t : R} {n : ℕ} (h : p ≠ 0) (hroot : ∀ m ≤ n, ((⇑derivative)^[m] p).IsRoot t) (hnzd : ↑n.factorial ∈ nonZeroDivisors R) :
n < rootMultiplicity t p
source
theorem Polynomial.lt_rootMultiplicity_of_isRoot_iterate_derivative_of_mem_nonZeroDivisors' {R : Type u} [CommRing R] {p : Polynomial R} {t : R} {n : ℕ} (h : p ≠ 0) (hroot : ∀ m ≤ n, ((⇑derivative)^[m] p).IsRoot t) (hnzd : ∀ m ≤ n, m ≠ 0 → ↑m ∈ nonZeroDivisors R) :
n < rootMultiplicity t p
source
theorem Polynomial.lt_rootMultiplicity_iff_isRoot_iterate_derivative_of_mem_nonZeroDivisors {R : Type u} [CommRing R] {p : Polynomial R} {t : R} {n : ℕ} (h : p ≠ 0) (hnzd : ↑n.factorial ∈ nonZeroDivisors R) :
n < rootMultiplicity t p ↔ ∀ m ≤ n, ((⇑derivative)^[m] p).IsRoot t
source
theorem Polynomial.lt_rootMultiplicity_iff_isRoot_iterate_derivative_of_mem_nonZeroDivisors' {R : Type u} [CommRing R] {p : Polynomial R} {t : R} {n : ℕ} (h : p ≠ 0) (hnzd : ∀ m ≤ n, m ≠ 0 → ↑m ∈ nonZeroDivisors R) :
n < rootMultiplicity t p ↔ ∀ m ≤ n, ((⇑derivative)^[m] p).IsRoot t
source
theorem Polynomial.one_lt_rootMultiplicity_iff_isRoot_iterate_derivative {R : Type u} [CommRing R] {p : Polynomial R} {t : R} (h : p ≠ 0) :
1 < rootMultiplicity t p ↔ ∀ m ≤ 1, ((⇑derivative)^[m] p).IsRoot t
source
theorem Polynomial.one_lt_rootMultiplicity_iff_isRoot {R : Type u} [CommRing R] {p : Polynomial R} {t : R} (h : p ≠ 0) :
1 < rootMultiplicity t p ↔ p.IsRoot t ∧ (derivative p).IsRoot t
source
theorem Polynomial.one_lt_rootMultiplicity_iff_isRoot_gcd {R : Type u} [CommRing R] [IsDomain R] [GCDMonoid (Polynomial R)] {p : Polynomial R} {t : R} (h : p ≠ 0) :
1 < rootMultiplicity t p ↔ (gcd p (derivative p)).IsRoot t
source
theorem Polynomial.derivative_rootMultiplicity_of_root {R : Type u} [CommRing R] [IsDomain R] [CharZero R] {p : Polynomial R} {t : R} (hpt : p.IsRoot t) :
rootMultiplicity t (derivative p) = rootMultiplicity t p - 1
source
theorem Polynomial.rootMultiplicity_sub_one_le_derivative_rootMultiplicity {R : Type u} [CommRing R] [IsDomain R] [CharZero R] (p : Polynomial R) (t : R) :
rootMultiplicity t p - 1 ≤ rootMultiplicity t (derivative p)
source
theorem Polynomial.lt_rootMultiplicity_of_isRoot_iterate_derivative {R : Type u} [CommRing R] [IsDomain R] [CharZero R] {p : Polynomial R} {t : R} {n : ℕ} (h : p ≠ 0) (hroot : ∀ m ≤ n, ((⇑derivative)^[m] p).IsRoot t) :
n < rootMultiplicity t p
source
theorem Polynomial.lt_rootMultiplicity_iff_isRoot_iterate_derivative {R : Type u} [CommRing R] [IsDomain R] [CharZero R] {p : Polynomial R} {t : R} {n : ℕ} (h : p ≠ 0) :
n < rootMultiplicity t p ↔ ∀ m ≤ n, ((⇑derivative)^[m] p).IsRoot t
source
theorem Polynomial.isRoot_of_isRoot_of_dvd_derivative_mul {R : Type u} [CommRing R] [IsDomain R] [CharZero R] {f g : Polynomial R} (hf0 : f ≠ 0) (hfd : f ∣ derivative f * g) {a : R} (haf : f.IsRoot a) :
g.IsRoot a

A sufficient condition for the set of roots of a nonzero polynomial `f` to be a subset of the set of roots of `g` is that `f` divides `f.derivative * g`. Over an algebraically closed field of characteristic zero, this is also a necessary condition. See `isRoot_of_isRoot_iff_dvd_derivative_mul`

source
instance Polynomial.instNormalizationMonoid {R : Type u} [CommRing R] [IsDomain R] [NormalizationMonoid R] :
NormalizationMonoid (Polynomial R)
Equations

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

source
@[simp]
theorem Polynomial.coe_normUnit {R : Type u} [CommRing R] [IsDomain R] [NormalizationMonoid R] {p : Polynomial R} :
↑(normUnit p) = C ↑(normUnit p.leadingCoeff)
source
@[simp]
theorem Polynomial.leadingCoeff_normalize {R : Type u} [CommRing R] [IsDomain R] [NormalizationMonoid R] (p : Polynomial R) :
(normalize p).leadingCoeff = normalize p.leadingCoeff
source
theorem Polynomial.Monic.normalize_eq_self {R : Type u} [CommRing R] [IsDomain R] [NormalizationMonoid R] {p : Polynomial R} (hp : p.Monic) :
normalize p = p
source
theorem Polynomial.roots_normalize {R : Type u} [CommRing R] [IsDomain R] [NormalizationMonoid R] {p : Polynomial R} :
(normalize p).roots = p.roots
source
theorem Polynomial.normUnit_X {R : Type u} [CommRing R] [IsDomain R] [NormalizationMonoid R] :
normUnit X = 1
source
theorem Polynomial.X_eq_normalize {R : Type u} [CommRing R] [IsDomain R] [NormalizationMonoid R] :
X = normalize X
source
theorem Polynomial.degree_pos_of_ne_zero_of_nonunit {R : Type u} [DivisionRing R] {p : Polynomial R} (hp0 : p ≠ 0) (hp : ¬IsUnit p) :
0 < p.degree
source
@[simp]
theorem Polynomial.map_eq_zero {R : Type u} {S : Type v} [Ring R] [IsSimpleRing R] [Semiring S] [Nontrivial S] {p : Polynomial R} (f : R →+* S) :
map f p = 0 ↔ p = 0
source
theorem Polynomial.map_ne_zero {R : Type u} {S : Type v} [Ring R] [IsSimpleRing R] [Semiring S] [Nontrivial S] {p : Polynomial R} {f : R →+* S} (hp : p ≠ 0) :
map f p ≠ 0
source
@[simp]
theorem Polynomial.degree_map {R : Type u} {S : Type v} [Ring R] [IsSimpleRing R] [Semiring S] [Nontrivial S] (p : Polynomial R) (f : R →+* S) :
(map f p).degree = p.degree
source
@[simp]
theorem Polynomial.natDegree_map {R : Type u} {S : Type v} [Ring R] [IsSimpleRing R] [Semiring S] [Nontrivial S] {p : Polynomial R} (f : R →+* S) :
(map f p).natDegree = p.natDegree
source
@[simp]
theorem Polynomial.leadingCoeff_map {R : Type u} {S : Type v} [Ring R] [IsSimpleRing R] [Semiring S] [Nontrivial S] {p : Polynomial R} (f : R →+* S) :
(map f p).leadingCoeff = f p.leadingCoeff
source
theorem Polynomial.nextCoeff_map_eq {R : Type u} {S : Type v} [Ring R] [IsSimpleRing R] [Semiring S] [Nontrivial S] (p : Polynomial R) (f : R →+* S) :
(map f p).nextCoeff = f p.nextCoeff
source
@[simp]
theorem Polynomial.monic_map_iff {R : Type u} {S : Type v} [Ring R] [IsSimpleRing R] [Semiring S] [Nontrivial S] {f : R →+* S} {p : Polynomial R} :
(map f p).Monic ↔ p.Monic
source
theorem Polynomial.isUnit_iff_degree_eq_zero {R : Type u} [Field R] {p : Polynomial R} :
IsUnit p ↔ p.degree = 0
source
def Polynomial.div {R : Type u} [Field R] (p q : Polynomial R) :
Polynomial R

Division of polynomials. See `Polynomial.divByMonic` for more details.

Equations

- p.div q = Polynomial.C q.leadingCoeff⁻¹ * (p /ₘ (q * Polynomial.C q.leadingCoeff⁻¹))

Instances For

source
def Polynomial.mod {R : Type u} [Field R] (p q : Polynomial R) :
Polynomial R

Remainder of polynomial division. See `Polynomial.modByMonic` for more details.

Equations

- p.mod q = p %ₘ (q * Polynomial.C q.leadingCoeff⁻¹)

Instances For

source
instance Polynomial.instDiv {R : Type u} [Field R] :
Div (Polynomial R)
Equations

- Polynomial.instDiv = { div := Polynomial.div }

source
instance Polynomial.instMod {R : Type u} [Field R] :
Mod (Polynomial R)
Equations

- Polynomial.instMod = { mod := Polynomial.mod }

source
theorem Polynomial.div_def {R : Type u} [Field R] {p q : Polynomial R} :
p / q = C q.leadingCoeff⁻¹ * (p /ₘ (q * C q.leadingCoeff⁻¹))
source
theorem Polynomial.mod_def {R : Type u} [Field R] {p q : Polynomial R} :
p % q = p %ₘ (q * C q.leadingCoeff⁻¹)
source
theorem Polynomial.modByMonic_eq_mod {R : Type u} [Field R] {q : Polynomial R} (p : Polynomial R) (hq : q.Monic) :
p %ₘ q = p % q
source
theorem Polynomial.divByMonic_eq_div {R : Type u} [Field R] {q : Polynomial R} (p : Polynomial R) (hq : q.Monic) :
p /ₘ q = p / q
source
theorem Polynomial.mod_X_sub_C_eq_C_eval {R : Type u} [Field R] (p : Polynomial R) (a : R) :
p % (X - C a) = C (eval a p)
source
theorem Polynomial.mul_div_eq_iff_isRoot {R : Type u} {a : R} [Field R] {p : Polynomial R} :
(X - C a) * (p / (X - C a)) = p ↔ p.IsRoot a
source
theorem Polynomial.IsRoot.mul_div_eq {R : Type u} {a : R} [Field R] {p : Polynomial R} :
p.IsRoot a → (X - C a) * (p / (X - C a)) = p

Alias of the reverse direction of `Polynomial.mul_div_eq_iff_isRoot`.

source
instance Polynomial.instEuclideanDomain {R : Type u} [Field R] :
EuclideanDomain (Polynomial R)
Equations

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

source
theorem Polynomial.mod_eq_self_iff {R : Type u} [Field R] {p q : Polynomial R} (hq0 : q ≠ 0) :
p % q = p ↔ p.degree < q.degree
source
theorem Polynomial.div_eq_zero_iff {R : Type u} [Field R] {p q : Polynomial R} (hq0 : q ≠ 0) :
p / q = 0 ↔ p.degree < q.degree
source
theorem Polynomial.degree_add_div {R : Type u} [Field R] {p q : Polynomial R} (hq0 : q ≠ 0) (hpq : q.degree ≤ p.degree) :
q.degree + (p / q).degree = p.degree
source
theorem Polynomial.degree_div_le {R : Type u} [Field R] (p q : Polynomial R) :
(p / q).degree ≤ p.degree
source
theorem Polynomial.degree_div_lt {R : Type u} [Field R] {p q : Polynomial R} (hp : p ≠ 0) (hq : 0 < q.degree) :
(p / q).degree < p.degree
source
theorem Polynomial.isUnit_map {R : Type u} {k : Type y} [Field R] {p : Polynomial R} [Field k] (f : R →+* k) :
IsUnit (map f p) ↔ IsUnit p
source
theorem Polynomial.map_div {R : Type u} {k : Type y} [Field R] {p q : Polynomial R} [Field k] (f : R →+* k) :
map f (p / q) = map f p / map f q
source
theorem Polynomial.map_mod {R : Type u} {k : Type y} [Field R] {p q : Polynomial R} [Field k] (f : R →+* k) :
map f (p % q) = map f p % map f q
source
theorem Polynomial.natDegree_mod_lt {k : Type y} [Field k] (p : Polynomial k) {q : Polynomial k} (hq : q.natDegree ≠ 0) :
(p % q).natDegree < q.natDegree
source
theorem Polynomial.gcd_map {R : Type u} {k : Type y} [Field R] {p q : Polynomial R} [Field k] [DecidableEq R] [DecidableEq k] (f : R →+* k) :
EuclideanDomain.gcd (map f p) (map f q) = map f (EuclideanDomain.gcd p q)
source
theorem Polynomial.eval₂_gcd_eq_zero {R : Type u} {k : Type y} [Field R] [CommSemiring k] [DecidableEq R] {ϕ : R →+* k} {f g : Polynomial R} {α : k} (hf : eval₂ ϕ α f = 0) (hg : eval₂ ϕ α g = 0) :
eval₂ ϕ α (EuclideanDomain.gcd f g) = 0
source
theorem Polynomial.eval_gcd_eq_zero {R : Type u} [Field R] [DecidableEq R] {f g : Polynomial R} {α : R} (hf : eval α f = 0) (hg : eval α g = 0) :
eval α (EuclideanDomain.gcd f g) = 0
source
theorem Polynomial.root_left_of_root_gcd {R : Type u} {k : Type y} [Field R] [CommSemiring k] [DecidableEq R] {ϕ : R →+* k} {f g : Polynomial R} {α : k} (hα : eval₂ ϕ α (EuclideanDomain.gcd f g) = 0) :
eval₂ ϕ α f = 0
source
theorem Polynomial.root_right_of_root_gcd {R : Type u} {k : Type y} [Field R] [CommSemiring k] [DecidableEq R] {ϕ : R →+* k} {f g : Polynomial R} {α : k} (hα : eval₂ ϕ α (EuclideanDomain.gcd f g) = 0) :
eval₂ ϕ α g = 0
source
theorem Polynomial.root_gcd_iff_root_left_right {R : Type u} {k : Type y} [Field R] [CommSemiring k] [DecidableEq R] {ϕ : R →+* k} {f g : Polynomial R} {α : k} :
eval₂ ϕ α (EuclideanDomain.gcd f g) = 0 ↔ eval₂ ϕ α f = 0 ∧ eval₂ ϕ α g = 0
source
theorem Polynomial.isRoot_gcd_iff_isRoot_left_right {R : Type u} [Field R] [DecidableEq R] {f g : Polynomial R} {α : R} :
(EuclideanDomain.gcd f g).IsRoot α ↔ f.IsRoot α ∧ g.IsRoot α
source
theorem Polynomial.isCoprime_map {R : Type u} {k : Type y} [Field R] {p q : Polynomial R} [Field k] (f : R →+* k) :
IsCoprime (map f p) (map f q) ↔ IsCoprime p q
source
theorem Polynomial.mem_roots_map {R : Type u} {k : Type y} [Field R] {p : Polynomial R} [CommRing k] [IsDomain k] {f : R →+* k} {x : k} (hp : p ≠ 0) :
x ∈ (map f p).roots ↔ eval₂ f x p = 0
source
theorem Polynomial.rootSet_monomial {R : Type u} {S : Type v} [Field R] [CommRing S] [IsDomain S] [Algebra R S] {n : ℕ} (hn : n ≠ 0) {a : R} (ha : a ≠ 0) :
((monomial n) a).rootSet S = {0}
source
theorem Polynomial.rootSet_C_mul_X_pow {R : Type u} {S : Type v} [Field R] [CommRing S] [IsDomain S] [Algebra R S] {n : ℕ} (hn : n ≠ 0) {a : R} (ha : a ≠ 0) :
(C a * X ^ n).rootSet S = {0}
source
theorem Polynomial.rootSet_X_pow {R : Type u} {S : Type v} [Field R] [CommRing S] [IsDomain S] [Algebra R S] {n : ℕ} (hn : n ≠ 0) :
(X ^ n).rootSet S = {0}
source
theorem Polynomial.rootSet_prod {R : Type u} {S : Type v} [Field R] [CommRing S] [IsDomain S] [Algebra R S] {ι : Type u_1} (f : ι → Polynomial R) (s : Finset ι) (h : s.prod f ≠ 0) :
(s.prod f).rootSet S = ⋃ i ∈ s, (f i).rootSet S
source
theorem Polynomial.roots_C_mul_X_sub_C {R : Type u} {a : R} [Field R] (b : R) (ha : a ≠ 0) :
(C a * X - C b).roots = {a⁻¹ * b}
source
theorem Polynomial.roots_C_mul_X_add_C {R : Type u} {a : R} [Field R] (b : R) (ha : a ≠ 0) :
(C a * X + C b).roots = {-(a⁻¹ * b)}
source
theorem Polynomial.roots_degree_eq_one {R : Type u} [Field R] {p : Polynomial R} (h : p.degree = 1) :
p.roots = {-((p.coeff 1)⁻¹ * p.coeff 0)}
source
theorem Polynomial.exists_root_of_degree_eq_one {R : Type u} [Field R] {p : Polynomial R} (h : p.degree = 1) :
∃ (x : R), p.IsRoot x
source
theorem Polynomial.coeff_inv_units {R : Type u} [Field R] (u : (Polynomial R)ˣ) (n : ℕ) :
((↑u).coeff n)⁻¹ = (↑u⁻¹).coeff n
source
theorem Polynomial.monic_normalize {R : Type u} [Field R] {p : Polynomial R} [DecidableEq R] (hp0 : p ≠ 0) :
(normalize p).Monic
source
theorem Polynomial.normalize_eq_self_iff_monic {R : Type u} [Field R] [DecidableEq R] {p : Polynomial R} (hp : p ≠ 0) :
normalize p = p ↔ p.Monic
source
theorem Polynomial.leadingCoeff_div {R : Type u} [Field R] {p q : Polynomial R} (hpq : q.degree ≤ p.degree) :
(p / q).leadingCoeff = p.leadingCoeff / q.leadingCoeff
source
theorem Polynomial.div_C_mul {R : Type u} {a : R} [Field R] {p q : Polynomial R} :
p / (C a * q) = C a⁻¹ * (p / q)
source
theorem Polynomial.div_C {R : Type u} {a : R} [Field R] {p : Polynomial R} :
p / C a = p * C a⁻¹
source
theorem Polynomial.C_div {R : Type u} {a b : R} [Field R] :
C (a / b) = C a / C b
source
theorem Polynomial.C_mul_dvd {R : Type u} {a : R} [Field R] {p q : Polynomial R} (ha : a ≠ 0) :
C a * p ∣ q ↔ p ∣ q
source
theorem Polynomial.dvd_C_mul {R : Type u} {a : R} [Field R] {p q : Polynomial R} (ha : a ≠ 0) :
p ∣ C a * q ↔ p ∣ q
source
theorem Polynomial.coe_normUnit_of_ne_zero {R : Type u} [Field R] {p : Polynomial R} [DecidableEq R] (hp : p ≠ 0) :
↑(normUnit p) = C p.leadingCoeff⁻¹
source
theorem Polynomial.map_dvd_map' {R : Type u} {k : Type y} [Field R] [Field k] (f : R →+* k) {x y : Polynomial R} :
map f x ∣ map f y ↔ x ∣ y
source
@[simp]
theorem Polynomial.degree_normalize {R : Type u} [Field R] {p : Polynomial R} [DecidableEq R] :
(normalize p).degree = p.degree
source
theorem Polynomial.prime_of_degree_eq_one {R : Type u} [Field R] {p : Polynomial R} (hp1 : p.degree = 1) :
Prime p
source
theorem Polynomial.irreducible_of_degree_eq_one {R : Type u} [Field R] {p : Polynomial R} (hp1 : p.degree = 1) :
Irreducible p
source
theorem Polynomial.not_irreducible_C {R : Type u} [Field R] (x : R) :
¬Irreducible (C x)
source
theorem Polynomial.degree_pos_of_irreducible {R : Type u} [Field R] {p : Polynomial R} (hp : Irreducible p) :
0 < p.degree
source
theorem Polynomial.X_sub_C_mul_divByMonic_eq_sub_modByMonic {K : Type u_1} [Ring K] (f : Polynomial K) (a : K) :
(X - C a) * (f /ₘ (X - C a)) = f - f %ₘ (X - C a)
source
theorem Polynomial.divByMonic_add_X_sub_C_mul_derivative_divByMonic_eq_derivative {K : Type u_1} [CommRing K] (f : Polynomial K) (a : K) :
f /ₘ (X - C a) + (X - C a) * derivative (f /ₘ (X - C a)) = derivative f
source
@[deprecated Polynomial.divByMonic_add_X_sub_C_mul_derivative_divByMonic_eq_derivative (since := "2025-07-08")]
theorem Polynomial.divByMonic_add_X_sub_C_mul_derivate_divByMonic_eq_derivative {K : Type u_1} [CommRing K] (f : Polynomial K) (a : K) :
f /ₘ (X - C a) + (X - C a) * derivative (f /ₘ (X - C a)) = derivative f

Alias of `Polynomial.divByMonic_add_X_sub_C_mul_derivative_divByMonic_eq_derivative`.

source
theorem Polynomial.X_sub_C_dvd_derivative_of_X_sub_C_dvd_divByMonic {K : Type u_1} [Field K] (f : Polynomial K) {a : K} (hf : X - C a ∣ f /ₘ (X - C a)) :
X - C a ∣ derivative f
source
theorem Polynomial.isCoprime_of_is_root_of_eval_derivative_ne_zero {K : Type u_1} [Field K] (f : Polynomial K) (a : K) (hf' : eval a (derivative f) ≠ 0) :
IsCoprime (X - C a) (f /ₘ (X - C a))

If `f` is a polynomial over a field, and `a : K` satisfies `f' a ≠ 0`, then `f / (X - a)` is coprime with `X - a`. Note that we do not assume `f a = 0`, because `f / (X - a) = (f - f a) / (X - a)`.

source
theorem Polynomial.irreducible_iff_degree_lt {R : Type u} [Field R] (p : Polynomial R) (hp0 : p ≠ 0) (hpu : ¬IsUnit p) :
Irreducible p ↔ ∀ (q : Polynomial R), q.degree ≤ ↑(p.natDegree / 2) → q ∣ p → IsUnit q

To check a polynomial over a field is irreducible, it suffices to check only for divisors that have smaller degree.

See also: `Polynomial.Monic.irreducible_iff_natDegree`.

source
theorem Polynomial.irreducible_iff_lt_natDegree_lt {R : Type u} [Field R] {p : Polynomial R} (hp0 : p ≠ 0) (hpu : ¬IsUnit p) :
Irreducible p ↔ ∀ (q : Polynomial R), q.Monic → q.natDegree ∈ Finset.Ioc 0 (p.natDegree / 2) → ¬q ∣ p

To check a polynomial `p` over a field is irreducible, it suffices to check there are no divisors of degree `0 < d ≤ degree p / 2`.

See also: `Polynomial.Monic.irreducible_iff_natDegree'`.

source
theorem Polynomial.leadingCoeff_mul_prod_normalizedFactors {R : Type u} [Field R] [DecidableEq R] (a : Polynomial R) :
C a.leadingCoeff * (UniqueFactorizationMonoid.normalizedFactors a).prod = a

The normalized factors of a polynomial over a field times its leading coefficient give the polynomial.

source
theorem Polynomial.mem_normalizedFactors_iff {R : Type u} [Field R] {p q : Polynomial R} [DecidableEq R] (hq : q ≠ 0) :
p ∈ UniqueFactorizationMonoid.normalizedFactors q ↔ Irreducible p ∧ p.Monic ∧ p ∣ q
source
@[simp]
theorem Polynomial.map_normalize {R : Type u} {S : Type v} [Field R] (p : Polynomial R) [DecidableEq R] [Field S] [DecidableEq S] (f : R →+* S) :
map f (normalize p) = normalize (map f p)
source
theorem Polynomial.monic_mapAlg_iff {R : Type u} {S : Type v} [Field R] [Semiring S] [Nontrivial S] [Algebra R S] {p : Polynomial R} :
((mapAlg R S) p).Monic ↔ p.Monic
source
theorem Irreducible.natDegree_pos {F : Type u_1} [DivisionSemiring F] {f : Polynomial F} (h : Irreducible f) :
0 < f.natDegree

An irreducible polynomial over a field must have positive degree.

source
theorem Irreducible.degree_pos {F : Type u_1} [DivisionSemiring F] {f : Polynomial F} (h : Irreducible f) :
0 < f.degree

An irreducible polynomial over a field must have positive degree.