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} :

theorem polynomial.ne_zero_of_monic_of_zero_ne_one {R : Type u} [semiring R] {p : polynomial R} :
p.monic0 1p 0

theorem polynomial.ne_zero_of_ne_zero_of_monic {R : Type u} [semiring R] {p q : polynomial R} :
p 0q.monicq 0

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

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

theorem polynomial.monic_X_pow_add {R : Type u} [semiring R] {p : polynomial R} {n : } :
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} :
p.monicq.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_prod_of_monic {R : Type u} {ι : Type y} [comm_semiring R] (s : finset ι) (f : ι → polynomial R) :
(∀ (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} :
p.monicis_unit pp = 1

theorem polynomial.monic.coeff_nat_degree {R : Type u} [comm_ring R] {p : polynomial R} :
p.monicp.coeff p.nat_degree = 1

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

theorem polynomial.monic.nat_degree_mul {R : Type u} [comm_ring R] [nontrivial R] {p q : polynomial R} :
p.monicq.monic(p * q).nat_degree = p.nat_degree + q.nat_degree

theorem polynomial.monic.next_coeff_mul {R : Type u} [comm_ring R] {p q : polynomial R} :
p.monicq.monic(p * q).next_coeff = p.next_coeff + q.next_coeff

theorem polynomial.monic.next_coeff_prod {R : Type u} {ι : Type y} [comm_ring R] (s : finset ι) (f : ι → polynomial R) :
(∀ (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 : } :
p.degree n(polynomial.X ^ (n + 1) - p).monic

theorem polynomial.monic_X_pow_sub_C {R : Type u} [ring R] (a : R) {n : } :

X ^ n - a is 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} :

@[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} :
p.monicp 0