Theory of monic polynomials

We give several tools for proving that polynomials are monic, e.g. Monic.mul, Monic.map, Monic.pow.

theorem Polynomial.monic_zero_iff_subsingleton {R : Type u} [Semiring R] : Monic 0 ↔ Subsingleton R

theorem Polynomial.not_monic_zero_iff {R : Type u} [Semiring R] : ¬Monic 0 ↔ 0 ≠ 1

theorem Polynomial.monic_zero_iff_subsingleton' {R : Type u} [Semiring R] : Monic 0 ↔ (∀ (f g : Polynomial R), f = g) ∧ ∀ (a b : R), a = b

theorem Polynomial.Monic.as_sum {R : Type u} [Semiring R] {p : Polynomial R} (hp : p.Monic) : p = X ^ p.natDegree + ∑ i ∈ Finset.range p.natDegree, C (p.coeff i) * X ^ i

theorem Polynomial.Monic.map {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] (f : R →+* S) (hp : p.Monic) : (Polynomial.map f p).Monic

theorem Polynomial.monic_C_mul_of_mul_leadingCoeff_eq_one {R : Type u} [Semiring R] {p : Polynomial R} {b : R} (hp : b * p.leadingCoeff = 1) : (C b * p).Monic

theorem Polynomial.monic_mul_C_of_leadingCoeff_mul_eq_one {R : Type u} [Semiring R] {p : Polynomial R} {b : R} (hp : p.leadingCoeff * b = 1) : (p * C b).Monic

theorem Polynomial.monic_X_pow_add {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} (H : p.degree < ↑n) : (X ^ n + p).Monic

theorem Polynomial.monic_X_pow_add_C {R : Type u} (a : R) [Semiring R] {n : ℕ} (h : n ≠ 0) : (X ^ n + C a).Monic

theorem Polynomial.monic_X_add_C {R : Type u} [Semiring R] (x : R) : (X + C x).Monic

theorem Polynomial.Monic.mul {R : Type u} [Semiring R] {p q : Polynomial R} (hp : p.Monic) (hq : q.Monic) : (p * q).Monic

theorem Polynomial.Monic.pow {R : Type u} [Semiring R] {p : Polynomial R} (hp : p.Monic) (n : ℕ) : (p ^ n).Monic

theorem Polynomial.Monic.add_of_left {R : Type u} [Semiring R] {p q : Polynomial R} (hp : p.Monic) (hpq : q.degree < p.degree) : (p + q).Monic

theorem Polynomial.Monic.add_of_right {R : Type u} [Semiring R] {p q : Polynomial R} (hq : q.Monic) (hpq : p.degree < q.degree) : (p + q).Monic

theorem Polynomial.Monic.of_mul_monic_left {R : Type u} [Semiring R] {p q : Polynomial R} (hp : p.Monic) (hpq : (p * q).Monic) : q.Monic

theorem Polynomial.Monic.of_mul_monic_right {R : Type u} [Semiring R] {p q : Polynomial R} (hq : q.Monic) (hpq : (p * q).Monic) : p.Monic

theorem Polynomial.Monic.comp {R : Type u} [Semiring R] {p q : Polynomial R} (hp : p.Monic) (hq : q.Monic) (h : q.natDegree ≠ 0) : (p.comp q).Monic

theorem Polynomial.Monic.comp_X_add_C {R : Type u} [Semiring R] {p : Polynomial R} (hp : p.Monic) (r : R) : (p.comp (X + C r)).Monic

@[deprecated Polynomial.Monic.natDegree_eq_zero (since := "2025-10-26")]

theorem Polynomial.Monic.natDegree_eq_zero_iff_eq_one {R : Type u} [Semiring R] {p : Polynomial R} (hf : p.Monic) : p.natDegree = 0 ↔ p = 1

Alias of Polynomial.Monic.natDegree_eq_zero.

@[simp]

theorem Polynomial.Monic.degree_le_zero_iff_eq_one {R : Type u} [Semiring R] {p : Polynomial R} (hp : p.Monic) : p.degree ≤ 0 ↔ p = 1

theorem Polynomial.Monic.natDegree_mul {R : Type u} [Semiring R] {p q : Polynomial R} (hp : p.Monic) (hq : q.Monic) : (p * q).natDegree = p.natDegree + q.natDegree

theorem Polynomial.Monic.degree_mul_comm {R : Type u} [Semiring R] {p : Polynomial R} (hp : p.Monic) (q : Polynomial R) : (p * q).degree = (q * p).degree

theorem Polynomial.Monic.natDegree_mul' {R : Type u} [Semiring R] {p q : Polynomial R} (hp : p.Monic) (hq : q ≠ 0) : (p * q).natDegree = p.natDegree + q.natDegree

theorem Polynomial.Monic.natDegree_mul_comm {R : Type u} [Semiring R] {p : Polynomial R} (hp : p.Monic) (q : Polynomial R) : (p * q).natDegree = (q * p).natDegree

theorem Polynomial.not_isUnit_X_add_C {R : Type u} [Semiring R] [Nontrivial R] (a : R) : ¬IsUnit (X + C a)

theorem Polynomial.Monic.not_dvd_of_natDegree_lt {R : Type u} [Semiring R] {p q : Polynomial R} (hp : p.Monic) (h0 : q ≠ 0) (hl : q.natDegree < p.natDegree) : ¬p ∣ q

theorem Polynomial.Monic.not_dvd_of_degree_lt {R : Type u} [Semiring R] {p q : Polynomial R} (hp : p.Monic) (h0 : q ≠ 0) (hl : q.degree < p.degree) : ¬p ∣ q

theorem Polynomial.Monic.nextCoeff_mul {R : Type u} [Semiring R] {p q : Polynomial R} (hp : p.Monic) (hq : q.Monic) : (p * q).nextCoeff = p.nextCoeff + q.nextCoeff

theorem Polynomial.Monic.nextCoeff_pow {R : Type u} [Semiring R] {p : Polynomial R} (hp : p.Monic) (n : ℕ) : (p ^ n).nextCoeff = n • p.nextCoeff

theorem Polynomial.Monic.eq_one_of_map_eq_one {R : Type u} [Semiring R] {p : Polynomial R} {S : Type u_1} [Semiring S] [Nontrivial S] (f : R →+* S) (hp : p.Monic) (map_eq : Polynomial.map f p = 1) : p = 1

theorem Polynomial.Monic.natDegree_pow {R : Type u} [Semiring R] {p : Polynomial R} (hp : p.Monic) (n : ℕ) : (p ^ n).natDegree = n * p.natDegree

@[simp]

theorem Polynomial.natDegree_pow_X_add_C {R : Type u} [Semiring R] [Nontrivial R] (n : ℕ) (r : R) : ((X + C r) ^ n).natDegree = n

theorem Polynomial.Monic.eq_one_of_isUnit {R : Type u} [Semiring R] {p : Polynomial R} (hm : p.Monic) (hpu : IsUnit p) : p = 1

theorem Polynomial.Monic.isUnit_iff {R : Type u} [Semiring R] {p : Polynomial R} (hm : p.Monic) : IsUnit p ↔ p = 1

theorem Polynomial.eq_of_monic_of_associated {R : Type u} [Semiring R] {p q : Polynomial R} (hp : p.Monic) (hq : q.Monic) (hpq : Associated p q) : p = q

@[reducible, inline]

abbrev Polynomial.MonicDegreeEq (R : Type u) (n : ℕ) [Semiring R] : Type u

The type of monic polynomials of degree n.

The implementation is slightly different because it is useful to still contain X ^ n when R is trivial. See MonicDegreeEq.mk for the usual constructor.

@[simp]

theorem Polynomial.MonicDegreeEq.natDegree {R : Type u} {n : ℕ} [Semiring R] [Nontrivial R] (p : MonicDegreeEq R n) : (↑p).natDegree = n

@[simp]

theorem Polynomial.MonicDegreeEq.degree {R : Type u} {n : ℕ} [Semiring R] [Nontrivial R] (p : MonicDegreeEq R n) : (↑p).degree = ↑n

theorem Polynomial.MonicDegreeEq.monic {R : Type u} {n : ℕ} [Semiring R] (p : MonicDegreeEq R n) : (↑p).Monic

theorem Polynomial.MonicDegreeEq.coeff_of_ge {R : Type u} {n : ℕ} [Semiring R] (p : MonicDegreeEq R n) (i : ℕ) (hi : n ≤ i) : (↑p).coeff i = if i = n then 1 else 0

def Polynomial.MonicDegreeEq.mk {R : Type u} {n : ℕ} [Semiring R] (p : Polynomial R) (hp : p.Monic) (hp' : p.natDegree = n) : MonicDegreeEq R n

The constructor for MonicDegreeEq given a monic polynomial of degree n.

@[simp]

theorem Polynomial.MonicDegreeEq.mk_coe {R : Type u} {n : ℕ} [Semiring R] (p : Polynomial R) (hp : p.Monic) (hp' : p.natDegree = n) : ↑(mk p hp hp') = p

noncomputable def Polynomial.MonicDegreeEq.map {R : Type u} {S : Type v} {n : ℕ} [Semiring R] [Semiring S] (p : MonicDegreeEq R n) (f : R →+* S) : MonicDegreeEq S n

The image of a monic polynomial of degree n under a ring homomorphism.

@[simp]

theorem Polynomial.MonicDegreeEq.map_coe {R : Type u} {S : Type v} {n : ℕ} [Semiring R] [Semiring S] (p : MonicDegreeEq R n) (f : R →+* S) : ↑(p.map f) = Polynomial.map f ↑p

theorem Polynomial.monic_multiset_prod_of_monic {R : Type u} {ι : Type y} [CommSemiring R] (t : Multiset ι) (f : ι → Polynomial R) (ht : ∀ i ∈ t, (f i).Monic) : (Multiset.map f t).prod.Monic

theorem Polynomial.monic_prod_of_monic {R : Type u} {ι : Type y} [CommSemiring R] (s : Finset ι) (f : ι → Polynomial R) (hs : ∀ i ∈ s, (f i).Monic) : (∏ i ∈ s, f i).Monic

theorem Polynomial.monic_finprod_of_monic {R : Type u} [CommSemiring R] (α : Type u_1) (f : α → Polynomial R) (hf : ∀ i ∈ Function.mulSupport f, (f i).Monic) : (finprod f).Monic

theorem Polynomial.Monic.nextCoeff_multiset_prod {R : Type u} {ι : Type y} [CommSemiring R] (t : Multiset ι) (f : ι → Polynomial R) (h : ∀ i ∈ t, (f i).Monic) : (Multiset.map f t).prod.nextCoeff = (Multiset.map (fun (i : ι) => (f i).nextCoeff) t).sum

theorem Polynomial.Monic.nextCoeff_prod {R : Type u} {ι : Type y} [CommSemiring R] (s : Finset ι) (f : ι → Polynomial R) (h : ∀ i ∈ s, (f i).Monic) : (∏ i ∈ s, f i).nextCoeff = ∑ i ∈ s, (f i).nextCoeff

theorem Polynomial.irreducible_of_monic {R : Type u} [CommSemiring R] [NoZeroDivisors R] {p : Polynomial R} (hp : p.Monic) (hp1 : p ≠ 1) : Irreducible p ↔ ∀ (f g : Polynomial R), f.Monic → g.Monic → f * g = p → f = 1 ∨ g = 1

theorem Polynomial.Monic.irreducible_iff_natDegree {R : Type u} [CommSemiring R] [NoZeroDivisors R] {p : Polynomial R} (hp : p.Monic) : Irreducible p ↔ p ≠ 1 ∧ ∀ (f g : Polynomial R), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0

theorem Polynomial.Monic.irreducible_iff_natDegree' {R : Type u} [CommSemiring R] [NoZeroDivisors R] {p : Polynomial R} (hp : p.Monic) : Irreducible p ↔ p ≠ 1 ∧ ∀ (f g : Polynomial R), f.Monic → g.Monic → f * g = p → g.natDegree ∉ Finset.Ioc 0 (p.natDegree / 2)

theorem Polynomial.Monic.irreducible_iff_lt_natDegree_lt {R : Type u} [CommSemiring R] [NoZeroDivisors R] {p : Polynomial R} (hp : p.Monic) (hp1 : p ≠ 1) : Irreducible p ↔ ∀ (q : Polynomial R), q.Monic → q.natDegree ∈ Finset.Ioc 0 (p.natDegree / 2) → ¬q ∣ p

Alternate phrasing of Polynomial.Monic.irreducible_iff_natDegree' where we only have to check one divisor at a time.

theorem Polynomial.Monic.not_irreducible_iff_exists_add_mul_eq_coeff {R : Type u} [CommSemiring R] [NoZeroDivisors R] {p : Polynomial R} (hm : p.Monic) (hnd : p.natDegree = 2) : ¬Irreducible p ↔ ∃ (c₁ : R) (c₂ : R), p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂

@[simp]

theorem Polynomial.Monic.natDegree_map {R : Type u} {S : Type v} [Semiring R] [Semiring S] [Nontrivial S] {P : Polynomial R} (hmo : P.Monic) (f : R →+* S) : (Polynomial.map f P).natDegree = P.natDegree

@[simp]

theorem Polynomial.Monic.degree_map {R : Type u} {S : Type v} [Semiring R] [Semiring S] [Nontrivial S] {P : Polynomial R} (hmo : P.Monic) (f : R →+* S) : (Polynomial.map f P).degree = P.degree

@[deprecated Polynomial.leadingCoeff_map_of_injective (since := "2025-10-26")]

theorem Polynomial.leadingCoeff_map' {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

Alias of Polynomial.leadingCoeff_map_of_injective.

@[deprecated Polynomial.leadingCoeff_map_of_injective (since := "2025-10-26")]

theorem Polynomial.leadingCoeff_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

Alias of Polynomial.leadingCoeff_map_of_injective.

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

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

theorem Polynomial.monic_X_sub_C {R : Type u} [Ring R] (x : R) : (X - C x).Monic

theorem Polynomial.monic_X_pow_sub {R : Type u} [Ring R] {p : Polynomial R} {n : ℕ} (H : p.degree < ↑n) : (X ^ n - p).Monic

theorem Polynomial.monic_X_pow_sub_C {R : Type u} [Ring R] (a : R) {n : ℕ} (h : n ≠ 0) : (X ^ n - C a).Monic

X ^ n - a is monic.

theorem Polynomial.not_isUnit_X_pow_sub_one (R : Type u_1) [Ring R] [Nontrivial R] (n : ℕ) : ¬IsUnit (X ^ n - 1)

theorem Polynomial.Monic.comp_X_sub_C {R : Type u} [Ring R] {p : Polynomial R} (hp : p.Monic) (r : R) : (p.comp (X - C r)).Monic

theorem Polynomial.Monic.sub_of_left {R : Type u} [Ring R] {p q : Polynomial R} (hp : p.Monic) (hpq : q.degree < p.degree) : (p - q).Monic

theorem Polynomial.Monic.sub_of_right {R : Type u} [Ring R] {p q : Polynomial R} (hq : q.leadingCoeff = -1) (hpq : p.degree < q.degree) : (p - q).Monic

@[simp]

theorem Polynomial.not_monic_zero {R : Type u} [Semiring R] [Nontrivial R] : ¬Monic 0

theorem Polynomial.Monic.mul_left_ne_zero {R : Type u} [Semiring R] {p : Polynomial R} (hp : p.Monic) {q : Polynomial R} (hq : q ≠ 0) : q * p ≠ 0

theorem Polynomial.Monic.mul_right_ne_zero {R : Type u} [Semiring R] {p : Polynomial R} (hp : p.Monic) {q : Polynomial R} (hq : q ≠ 0) : p * q ≠ 0

theorem Polynomial.Monic.mul_natDegree_lt_iff {R : Type u} [Semiring R] {p : Polynomial R} (h : p.Monic) {q : Polynomial R} : (p * q).natDegree < p.natDegree ↔ p ≠ 1 ∧ q = 0

theorem Polynomial.Monic.mul_right_eq_zero_iff {R : Type u} [Semiring R] {p : Polynomial R} (h : p.Monic) {q : Polynomial R} : p * q = 0 ↔ q = 0

theorem Polynomial.Monic.mul_left_eq_zero_iff {R : Type u} [Semiring R] {p : Polynomial R} (h : p.Monic) {q : Polynomial R} : q * p = 0 ↔ q = 0

theorem Polynomial.Monic.isRegular {R : Type u_1} [Ring R] {p : Polynomial R} (hp : p.Monic) : IsRegular p

theorem Polynomial.degree_smul_of_smul_regular {R : Type u} [Semiring R] {S : Type u_1} [SMulZeroClass S R] {k : S} (p : Polynomial R) (h : IsSMulRegular R k) : (k • p).degree = p.degree

theorem Polynomial.natDegree_smul_of_smul_regular {R : Type u} [Semiring R] {S : Type u_1} [SMulZeroClass S R] {k : S} (p : Polynomial R) (h : IsSMulRegular R k) : (k • p).natDegree = p.natDegree

theorem Polynomial.leadingCoeff_smul_of_smul_regular {R : Type u} [Semiring R] {S : Type u_1} [SMulZeroClass S R] {k : S} (p : Polynomial R) (h : IsSMulRegular R k) : (k • p).leadingCoeff = k • p.leadingCoeff

theorem Polynomial.monic_of_isUnit_leadingCoeff_inv_smul {R : Type u} [Semiring R] {p : Polynomial R} (h : IsUnit p.leadingCoeff) : (h.unit⁻¹ • p).Monic

theorem Polynomial.isUnit_leadingCoeff_mul_right_eq_zero_iff {R : Type u} [Semiring R] {p : Polynomial R} (h : IsUnit p.leadingCoeff) {q : Polynomial R} : p * q = 0 ↔ q = 0

theorem Polynomial.isUnit_leadingCoeff_mul_left_eq_zero_iff {R : Type u} [Semiring R] {p : Polynomial R} (h : IsUnit p.leadingCoeff) {q : Polynomial R} : q * p = 0 ↔ q = 0