mathlib documentation

data.polynomial.monic

Theory of monic polynomials

We give several tools for proving that polynomials are monic, e.g. monic_mul, monic_map.

theorem polynomial.monic.as_sum {R : Type u} [semiring R] {p : polynomial R} (hp : p.monic) :

theorem polynomial.ne_zero_of_monic_of_zero_ne_one {R : Type u} [semiring R] {p : polynomial R} (hp : p.monic) (h : 0 1) :
p 0

theorem polynomial.ne_zero_of_ne_zero_of_monic {R : Type u} [semiring R] {p q : polynomial R} (hp : p 0) (hq : q.monic) :
q 0

theorem polynomial.monic_map {R : Type u} {S : Type v} [semiring R] {p : polynomial R} [semiring S] (f : R →+* S) (hp : p.monic) :

theorem polynomial.monic_mul_C_of_leading_coeff_mul_eq_one {R : Type u} [semiring R] {p : polynomial R} [nontrivial R] {b : R} (hp : (p.leading_coeff) * b = 1) :

theorem polynomial.monic_of_degree_le {R : Type u} [semiring R] {p : polynomial R} (n : ) (H1 : p.degree n) (H2 : p.coeff n = 1) :

theorem polynomial.monic_X_pow_add {R : Type u} [semiring R] {p : polynomial R} {n : } (H : p.degree n) :
(polynomial.X ^ (n + 1) + p).monic

theorem polynomial.monic_X_add_C {R : Type u} [semiring R] (x : R) :

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

@[simp]
theorem polynomial.monic.degree_eq_zero_iff_eq_one {R : Type u} [semiring R] {p : polynomial R} (hp : p.monic) :
p.nat_degree = 0 p = 1

theorem polynomial.monic.nat_degree_mul {R : Type u} [semiring R] {p q : polynomial R} (hp : p.monic) (hq : q.monic) :

theorem polynomial.monic.next_coeff_mul {R : Type u} [semiring R] {p q : polynomial R} (hp : p.monic) (hq : q.monic) :

theorem polynomial.monic_prod_of_monic {R : Type u} {ι : Type y} [comm_semiring R] (s : finset ι) (f : ι → polynomial R) (hs : ∀ (i : ι), i s(f i).monic) :
(∏ (i : ι) in s, f i).monic

theorem polynomial.is_unit_C {R : Type u} [comm_semiring R] {x : R} :

theorem polynomial.eq_one_of_is_unit_of_monic {R : Type u} [comm_semiring R] {p : polynomial R} (hm : p.monic) (hpu : is_unit p) :
p = 1

theorem polynomial.monic.next_coeff_prod {R : Type u} {ι : Type y} [comm_semiring R] (s : finset ι) (f : ι → polynomial R) (h : ∀ (i : ι), i s(f i).monic) :
(∏ (i : ι) in s, f i).next_coeff = ∑ (i : ι) in s, (f i).next_coeff

theorem polynomial.monic_X_sub_C {R : Type u} [ring R] (x : R) :

theorem polynomial.monic_X_pow_sub {R : Type u} [ring R] {p : polynomial R} {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) :

X ^ n - a is 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.leading_coeff = -1) (hpq : p.degree < q.degree) :
(p - q).monic

theorem polynomial.leading_coeff_of_injective {R : Type u} {S : Type v} [ring R] [semiring S] {f : R →+* S} (hf : function.injective f) (p : polynomial R) :

theorem polynomial.monic_of_injective {R : Type u} {S : Type v} [ring R] [semiring S] {f : R →+* S} (hf : function.injective f) {p : polynomial R} (hp : (polynomial.map f p).monic) :

@[simp]
theorem polynomial.not_monic_zero {R : Type u} [semiring R] [nontrivial R] :

theorem polynomial.ne_zero_of_monic {R : Type u} [semiring R] [nontrivial R] {p : polynomial R} (h : p.monic) :
p 0