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} [Semiring R] :
Polynomial.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 : Polynomial.Monic p) :
p = Polynomial.X ^ Polynomial.natDegree p + Finset.sum (Finset.range (Polynomial.natDegree p)) fun i => Polynomial.C (Polynomial.coeff p i) * Polynomial.X ^ i
theorem Polynomial.ne_zero_of_ne_zero_of_monic {R : Type u} [Semiring R] {p : Polynomial R} {q : Polynomial R} (hp : p 0) (hq : Polynomial.Monic q) :
q 0
theorem Polynomial.Monic.map {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] (f : R →+* S) (hp : Polynomial.Monic p) :
theorem Polynomial.monic_C_mul_of_mul_leadingCoeff_eq_one {R : Type u} [Semiring R] {p : Polynomial R} {b : R} (hp : b * Polynomial.leadingCoeff p = 1) :
Polynomial.Monic (Polynomial.C b * p)
theorem Polynomial.monic_mul_C_of_leadingCoeff_mul_eq_one {R : Type u} [Semiring R] {p : Polynomial R} {b : R} (hp : Polynomial.leadingCoeff p * b = 1) :
Polynomial.Monic (p * Polynomial.C b)
theorem Polynomial.monic_X_pow_add {R : Type u} [Semiring R] {p : Polynomial R} {n : } (H : Polynomial.degree p n) :
Polynomial.Monic (Polynomial.X ^ (n + 1) + p)
theorem Polynomial.monic_X_add_C {R : Type u} [Semiring R] (x : R) :
Polynomial.Monic (Polynomial.X + Polynomial.C x)
theorem Polynomial.Monic.pow {R : Type u} [Semiring R] {p : Polynomial R} (hp : Polynomial.Monic p) (n : ) :
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 : Polynomial.Monic p) (map_eq : Polynomial.map f p = 1) :
p = 1
@[simp]
theorem Polynomial.natDegree_pow_X_add_C {R : Type u} [Semiring R] [Nontrivial R] (n : ) (r : R) :
Polynomial.natDegree ((Polynomial.X + Polynomial.C r) ^ n) = n
theorem Polynomial.Monic.eq_one_of_isUnit {R : Type u} [Semiring R] {p : Polynomial R} (hm : Polynomial.Monic p) (hpu : IsUnit p) :
p = 1
theorem Polynomial.monic_multiset_prod_of_monic {R : Type u} {ι : Type y} [CommSemiring R] (t : Multiset ι) (f : ιPolynomial R) (ht : ∀ (i : ι), i tPolynomial.Monic (f i)) :
theorem Polynomial.monic_prod_of_monic {R : Type u} {ι : Type y} [CommSemiring R] (s : Finset ι) (f : ιPolynomial R) (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} [CommSemiring R] (t : Multiset ι) (f : ιPolynomial R) (h : ∀ (i : ι), i tPolynomial.Monic (f i)) :
theorem Polynomial.Monic.nextCoeff_prod {R : Type u} {ι : Type y} [CommSemiring R] (s : Finset ι) (f : ιPolynomial R) (h : ∀ (i : ι), i sPolynomial.Monic (f i)) :
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 : Polynomial R} {n : } (H : Polynomial.degree p n) :
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) [CommRing R] [Nontrivial R] (n : ) :
¬IsUnit (Polynomial.X ^ n - 1)
theorem Polynomial.Monic.mul_left_ne_zero {R : Type u} [Semiring R] {p : Polynomial R} (hp : Polynomial.Monic p) {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 : Polynomial.Monic p) {q : Polynomial R} (hq : q 0) :
p * q 0