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

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 : p.Monic) (hpq : q.degree < p.degree) :
(p - q).Monic
theorem Polynomial.Monic.sub_of_right {R : Type u} [Ring R] {p : } {q : } (hq : q.leadingCoeff = -1) (hpq : p.degree < q.degree) :
(p - q).Monic
@[simp]
theorem Polynomial.not_monic_zero {R : Type u} [] [] :
theorem Polynomial.Monic.mul_left_ne_zero {R : Type u} [] {p : } (hp : p.Monic) {q : } (hq : q 0) :
q * p 0
theorem Polynomial.Monic.mul_right_ne_zero {R : Type u} [] {p : } (hp : p.Monic) {q : } (hq : q 0) :
p * q 0
theorem Polynomial.Monic.mul_natDegree_lt_iff {R : Type u} [] {p : } (h : p.Monic) {q : } :
(p * q).natDegree < p.natDegree p 1 q = 0
theorem Polynomial.Monic.mul_right_eq_zero_iff {R : Type u} [] {p : } (h : p.Monic) {q : } :
p * q = 0 q = 0
theorem Polynomial.Monic.mul_left_eq_zero_iff {R : Type u} [] {p : } (h : p.Monic) {q : } :
q * p = 0 q = 0
theorem Polynomial.Monic.isRegular {R : Type u_1} [Ring R] {p : } (hp : p.Monic) :
theorem Polynomial.degree_smul_of_smul_regular {R : Type u} [] {S : Type u_1} [] [] {k : S} (p : ) (h : ) :
(k p).degree = p.degree
theorem Polynomial.natDegree_smul_of_smul_regular {R : Type u} [] {S : Type u_1} [] [] {k : S} (p : ) (h : ) :
(k p).natDegree = p.natDegree
theorem Polynomial.leadingCoeff_smul_of_smul_regular {R : Type u} [] {S : Type u_1} [] [] {k : S} (p : ) (h : ) :