# Documentation

Mathlib.Data.Polynomial.Monic

# 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} [] :
(∀ (f g : ), f = g) ∀ (a b : R), a = b
theorem Polynomial.Monic.as_sum {R : Type u} [] {p : } (hp : ) :
p = Polynomial.X ^ + Finset.sum () fun i => Polynomial.C () * Polynomial.X ^ i
theorem Polynomial.ne_zero_of_ne_zero_of_monic {R : Type u} [] {p : } {q : } (hp : p 0) (hq : ) :
q 0
theorem Polynomial.Monic.map {R : Type u} {S : Type v} [] {p : } [] (f : R →+* S) (hp : ) :
theorem Polynomial.monic_C_mul_of_mul_leadingCoeff_eq_one {R : Type u} [] {p : } {b : R} (hp : ) :
Polynomial.Monic (Polynomial.C b * p)
theorem Polynomial.monic_mul_C_of_leadingCoeff_mul_eq_one {R : Type u} [] {p : } {b : R} (hp : ) :
Polynomial.Monic (p * Polynomial.C b)
theorem Polynomial.monic_of_degree_le {R : Type u} [] {p : } (n : ) (H1 : ) (H2 : = 1) :
theorem Polynomial.monic_X_pow_add {R : Type u} [] {p : } {n : } (H : ) :
Polynomial.Monic (Polynomial.X ^ (n + 1) + p)
theorem Polynomial.monic_X_add_C {R : Type u} [] (x : R) :
Polynomial.Monic (Polynomial.X + Polynomial.C x)
theorem Polynomial.Monic.mul {R : Type u} [] {p : } {q : } (hp : ) (hq : ) :
theorem Polynomial.Monic.pow {R : Type u} [] {p : } (hp : ) (n : ) :
theorem Polynomial.Monic.add_of_left {R : Type u} [] {p : } {q : } (hp : ) (hpq : ) :
theorem Polynomial.Monic.add_of_right {R : Type u} [] {p : } {q : } (hq : ) (hpq : ) :
theorem Polynomial.Monic.of_mul_monic_left {R : Type u} [] {p : } {q : } (hp : ) (hpq : Polynomial.Monic (p * q)) :
theorem Polynomial.Monic.of_mul_monic_right {R : Type u} [] {p : } {q : } (hq : ) (hpq : Polynomial.Monic (p * q)) :
@[simp]
theorem Polynomial.Monic.natDegree_eq_zero_iff_eq_one {R : Type u} [] {p : } (hp : ) :
p = 1
@[simp]
theorem Polynomial.Monic.degree_le_zero_iff_eq_one {R : Type u} [] {p : } (hp : ) :
p = 1
theorem Polynomial.Monic.natDegree_mul {R : Type u} [] {p : } {q : } (hp : ) (hq : ) :
theorem Polynomial.Monic.degree_mul_comm {R : Type u} [] {p : } (hp : ) (q : ) :
theorem Polynomial.Monic.natDegree_mul' {R : Type u} [] {p : } {q : } (hp : ) (hq : q 0) :
theorem Polynomial.Monic.natDegree_mul_comm {R : Type u} [] {p : } (hp : ) (q : ) :
theorem Polynomial.Monic.not_dvd_of_natDegree_lt {R : Type u} [] {p : } {q : } (hp : ) (h0 : q 0) (hl : ) :
¬p q
theorem Polynomial.Monic.not_dvd_of_degree_lt {R : Type u} [] {p : } {q : } (hp : ) (h0 : q 0) (hl : ) :
¬p q
theorem Polynomial.Monic.nextCoeff_mul {R : Type u} [] {p : } {q : } (hp : ) (hq : ) :
theorem Polynomial.Monic.eq_one_of_map_eq_one {R : Type u} [] {p : } {S : Type u_1} [] [] (f : R →+* S) (hp : ) (map_eq : = 1) :
p = 1
theorem Polynomial.Monic.natDegree_pow {R : Type u} [] {p : } (hp : ) (n : ) :
@[simp]
theorem Polynomial.natDegree_pow_X_add_C {R : Type u} [] [] (n : ) (r : R) :
Polynomial.natDegree ((Polynomial.X + Polynomial.C r) ^ n) = n
theorem Polynomial.Monic.eq_one_of_isUnit {R : Type u} [] {p : } (hm : ) (hpu : ) :
p = 1
theorem Polynomial.Monic.isUnit_iff {R : Type u} [] {p : } (hm : ) :
p = 1
theorem Polynomial.monic_multiset_prod_of_monic {R : Type u} {ι : Type y} [] (t : ) (f : ι) (ht : ∀ (i : ι), i tPolynomial.Monic (f i)) :
theorem Polynomial.monic_prod_of_monic {R : Type u} {ι : Type y} [] (s : ) (f : ι) (hs : ∀ (i : ι), i sPolynomial.Monic (f i)) :
Polynomial.Monic (Finset.prod s fun i => f i)
theorem Polynomial.Monic.nextCoeff_multiset_prod {R : Type u} {ι : Type y} [] (t : ) (f : ι) (h : ∀ (i : ι), i tPolynomial.Monic (f i)) :
theorem Polynomial.Monic.nextCoeff_prod {R : Type u} {ι : Type y} [] (s : ) (f : ι) (h : ∀ (i : ι), i sPolynomial.Monic (f i)) :
@[simp]
theorem Polynomial.Monic.natDegree_map {R : Type u} {S : Type v} [] [] [] {P : } (hmo : ) (f : R →+* S) :
@[simp]
theorem Polynomial.Monic.degree_map {R : Type u} {S : Type v} [] [] [] {P : } (hmo : ) (f : R →+* S) :
theorem Polynomial.degree_map_eq_of_injective {R : Type u} {S : Type v} [] [] {f : R →+* S} (hf : ) (p : ) :
theorem Polynomial.natDegree_map_eq_of_injective {R : Type u} {S : Type v} [] [] {f : R →+* S} (hf : ) (p : ) :
theorem Polynomial.leadingCoeff_map' {R : Type u} {S : Type v} [] [] {f : R →+* S} (hf : ) (p : ) :
theorem Polynomial.nextCoeff_map {R : Type u} {S : Type v} [] [] {f : R →+* S} (hf : ) (p : ) :
= f ()
theorem Polynomial.leadingCoeff_of_injective {R : Type u} {S : Type v} [] [] {f : R →+* S} (hf : ) (p : ) :
theorem Polynomial.monic_of_injective {R : Type u} {S : Type v} [] [] {f : R →+* S} (hf : ) {p : } (hp : ) :
theorem Function.Injective.monic_map_iff {R : Type u} {S : Type v} [] [] {f : R →+* S} (hf : ) {p : } :
theorem Polynomial.monic_X_sub_C {R : Type u} [Ring R] (x : R) :
Polynomial.Monic (Polynomial.X - Polynomial.C x)
theorem Polynomial.monic_X_pow_sub {R : Type u} [Ring R] {p : } {n : } (H : ) :
Polynomial.Monic (Polynomial.X ^ (n + 1) - p)
theorem Polynomial.monic_X_pow_sub_C {R : Type u} [Ring R] (a : R) {n : } (h : n 0) :
Polynomial.Monic (Polynomial.X ^ n - Polynomial.C a)

X ^ n - a is monic.

theorem Polynomial.not_isUnit_X_pow_sub_one (R : Type u_1) [] [] (n : ) :
¬IsUnit (Polynomial.X ^ n - 1)
theorem Polynomial.Monic.sub_of_left {R : Type u} [Ring R] {p : } {q : } (hp : ) (hpq : ) :
theorem Polynomial.Monic.sub_of_right {R : Type u} [Ring R] {p : } {q : } (hq : ) (hpq : ) :
@[simp]
theorem Polynomial.not_monic_zero {R : Type u} [] [] :
theorem Polynomial.Monic.mul_left_ne_zero {R : Type u} [] {p : } (hp : ) {q : } (hq : q 0) :
q * p 0
theorem Polynomial.Monic.mul_right_ne_zero {R : Type u} [] {p : } (hp : ) {q : } (hq : q 0) :
p * q 0
theorem Polynomial.Monic.mul_natDegree_lt_iff {R : Type u} [] {p : } (h : ) {q : } :
p 1 q = 0
theorem Polynomial.Monic.mul_right_eq_zero_iff {R : Type u} [] {p : } (h : ) {q : } :
p * q = 0 q = 0
theorem Polynomial.Monic.mul_left_eq_zero_iff {R : Type u} [] {p : } (h : ) {q : } :
q * p = 0 q = 0
theorem Polynomial.Monic.isRegular {R : Type u_1} [Ring R] {p : } (hp : ) :
theorem Polynomial.degree_smul_of_smul_regular {R : Type u} [] {S : Type u_1} [] [] {k : S} (p : ) (h : ) :
theorem Polynomial.natDegree_smul_of_smul_regular {R : Type u} [] {S : Type u_1} [] [] {k : S} (p : ) (h : ) :
theorem Polynomial.leadingCoeff_smul_of_smul_regular {R : Type u} [] {S : Type u_1} [] [] {k : S} (p : ) (h : ) :
theorem Polynomial.isUnit_leadingCoeff_mul_right_eq_zero_iff {R : Type u} [] {p : } (h : ) {q : } :
p * q = 0 q = 0
theorem Polynomial.isUnit_leadingCoeff_mul_left_eq_zero_iff {R : Type u} [] {p : } (h : ) {q : } :
q * p = 0 q = 0