Documentation

Mathlib.Algebra.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 : 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} [Semiring R] {p : Polynomial R} {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) :
(Polynomial.map f p).Monic
theorem Polynomial.monic_C_mul_of_mul_leadingCoeff_eq_one {R : Type u} [Semiring R] {p : Polynomial R} {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} [Semiring R] {p : Polynomial R} {b : R} (hp : p.leadingCoeff * b = 1) :
(p * Polynomial.C b).Monic
theorem Polynomial.monic_of_degree_le {R : Type u} [Semiring R] {p : Polynomial R} (n : ) (H1 : p.degree n) (H2 : p.coeff n = 1) :
p.Monic
theorem Polynomial.monic_X_pow_add {R : Type u} [Semiring R] {p : Polynomial R} {n : } (H : p.degree < n) :
(Polynomial.X ^ n + p).Monic
theorem Polynomial.monic_X_pow_add_C {R : Type u} (a : R) [Semiring R] {n : } (h : n 0) :
(Polynomial.X ^ n + Polynomial.C a).Monic
theorem Polynomial.monic_X_add_C {R : Type u} [Semiring R] (x : R) :
(Polynomial.X + Polynomial.C x).Monic
theorem Polynomial.Monic.mul {R : Type u} [Semiring R] {p : Polynomial R} {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 : Polynomial R} {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 : Polynomial R} {q : Polynomial R} (hq : q.Monic) (hpq : p.degree < q.degree) :
(p + q).Monic
theorem Polynomial.Monic.of_mul_monic_left {R : Type u} [Semiring R] {p : Polynomial R} {q : Polynomial R} (hp : p.Monic) (hpq : (p * q).Monic) :
q.Monic
theorem Polynomial.Monic.of_mul_monic_right {R : Type u} [Semiring R] {p : Polynomial R} {q : Polynomial R} (hq : q.Monic) (hpq : (p * q).Monic) :
p.Monic
@[simp]
theorem Polynomial.Monic.natDegree_eq_zero_iff_eq_one {R : Type u} [Semiring R] {p : Polynomial R} (hp : p.Monic) :
p.natDegree = 0 p = 1
@[simp]
theorem Polynomial.Monic.degree_le_zero_iff_eq_one {R : Type u} [Semiring R] {p : Polynomial R} (hp : p.Monic) :
p.degree 0 p = 1
theorem Polynomial.Monic.natDegree_mul {R : Type u} [Semiring R] {p : Polynomial R} {q : Polynomial R} (hp : p.Monic) (hq : q.Monic) :
(p * q).natDegree = p.natDegree + q.natDegree
theorem Polynomial.Monic.degree_mul_comm {R : Type u} [Semiring R] {p : Polynomial R} (hp : p.Monic) (q : Polynomial R) :
(p * q).degree = (q * p).degree
theorem Polynomial.Monic.natDegree_mul' {R : Type u} [Semiring R] {p : Polynomial R} {q : Polynomial R} (hp : p.Monic) (hq : q 0) :
(p * q).natDegree = p.natDegree + q.natDegree
theorem Polynomial.Monic.natDegree_mul_comm {R : Type u} [Semiring R] {p : Polynomial R} (hp : p.Monic) (q : Polynomial R) :
(p * q).natDegree = (q * p).natDegree
theorem Polynomial.Monic.not_dvd_of_natDegree_lt {R : Type u} [Semiring R] {p : Polynomial R} {q : Polynomial R} (hp : p.Monic) (h0 : q 0) (hl : q.natDegree < p.natDegree) :
¬p q
theorem Polynomial.Monic.not_dvd_of_degree_lt {R : Type u} [Semiring R] {p : Polynomial R} {q : Polynomial R} (hp : p.Monic) (h0 : q 0) (hl : q.degree < p.degree) :
¬p q
theorem Polynomial.Monic.nextCoeff_mul {R : Type u} [Semiring R] {p : Polynomial R} {q : Polynomial R} (hp : p.Monic) (hq : q.Monic) :
(p * q).nextCoeff = p.nextCoeff + q.nextCoeff
theorem Polynomial.Monic.nextCoeff_pow {R : Type u} [Semiring R] {p : Polynomial R} (hp : p.Monic) (n : ) :
(p ^ n).nextCoeff = n p.nextCoeff
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 : p.Monic) (map_eq : Polynomial.map f p = 1) :
p = 1
theorem Polynomial.Monic.natDegree_pow {R : Type u} [Semiring R] {p : Polynomial R} (hp : p.Monic) (n : ) :
(p ^ n).natDegree = n * p.natDegree
@[simp]
theorem Polynomial.natDegree_pow_X_add_C {R : Type u} [Semiring R] [Nontrivial R] (n : ) (r : R) :
((Polynomial.X + Polynomial.C r) ^ n).natDegree = n
theorem Polynomial.Monic.eq_one_of_isUnit {R : Type u} [Semiring R] {p : Polynomial R} (hm : p.Monic) (hpu : IsUnit p) :
p = 1
theorem Polynomial.Monic.isUnit_iff {R : Type u} [Semiring R] {p : Polynomial R} (hm : p.Monic) :
IsUnit p p = 1
theorem Polynomial.eq_of_monic_of_associated {R : Type u} [Semiring R] {p : Polynomial R} {q : Polynomial R} (hp : p.Monic) (hq : q.Monic) (hpq : Associated p q) :
p = q
theorem Polynomial.monic_multiset_prod_of_monic {R : Type u} {ι : Type y} [CommSemiring R] (t : Multiset ι) (f : ιPolynomial R) (ht : it, (f i).Monic) :
(Multiset.map f t).prod.Monic
theorem Polynomial.monic_prod_of_monic {R : Type u} {ι : Type y} [CommSemiring R] (s : Finset ι) (f : ιPolynomial R) (hs : is, (f i).Monic) :
(∏ is, f i).Monic
theorem Polynomial.Monic.nextCoeff_multiset_prod {R : Type u} {ι : Type y} [CommSemiring R] (t : Multiset ι) (f : ιPolynomial R) (h : it, (f i).Monic) :
(Multiset.map f t).prod.nextCoeff = (Multiset.map (fun (i : ι) => (f i).nextCoeff) t).sum
theorem Polynomial.Monic.nextCoeff_prod {R : Type u} {ι : Type y} [CommSemiring R] (s : Finset ι) (f : ιPolynomial R) (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} [Semiring R] [Semiring S] [Nontrivial S] {P : Polynomial R} (hmo : P.Monic) (f : R →+* S) :
(Polynomial.map f P).natDegree = P.natDegree
@[simp]
theorem Polynomial.Monic.degree_map {R : Type u} {S : Type v} [Semiring R] [Semiring S] [Nontrivial S] {P : Polynomial R} (hmo : P.Monic) (f : R →+* S) :
(Polynomial.map f P).degree = P.degree
theorem Polynomial.degree_map_eq_of_injective {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} (hf : Function.Injective f) (p : Polynomial R) :
(Polynomial.map f p).degree = p.degree
theorem Polynomial.natDegree_map_eq_of_injective {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} (hf : Function.Injective f) (p : Polynomial R) :
(Polynomial.map f p).natDegree = p.natDegree
theorem Polynomial.leadingCoeff_map' {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} (hf : Function.Injective f) (p : Polynomial R) :
(Polynomial.map f p).leadingCoeff = f p.leadingCoeff
theorem Polynomial.nextCoeff_map {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} (hf : Function.Injective f) (p : Polynomial R) :
(Polynomial.map f p).nextCoeff = f p.nextCoeff
theorem Polynomial.leadingCoeff_of_injective {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} (hf : Function.Injective f) (p : Polynomial R) :
(Polynomial.map f p).leadingCoeff = f p.leadingCoeff
theorem Polynomial.monic_of_injective {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} (hf : Function.Injective f) {p : Polynomial R} (hp : (Polynomial.map f p).Monic) :
p.Monic
theorem Function.Injective.monic_map_iff {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} (hf : Function.Injective f) {p : Polynomial R} :
p.Monic (Polynomial.map f p).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 : Polynomial R} {n : } (H : p.degree < n) :
(Polynomial.X ^ n - 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) [CommRing R] [Nontrivial R] (n : ) :
¬IsUnit (Polynomial.X ^ n - 1)
theorem Polynomial.Monic.sub_of_left {R : Type u} [Ring R] {p : Polynomial R} {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 : Polynomial R} {q : Polynomial R} (hq : q.leadingCoeff = -1) (hpq : p.degree < q.degree) :
(p - q).Monic
theorem Polynomial.Monic.mul_left_ne_zero {R : Type u} [Semiring R] {p : Polynomial R} (hp : p.Monic) {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 : p.Monic) {q : Polynomial R} (hq : q 0) :
p * q 0
theorem Polynomial.Monic.mul_natDegree_lt_iff {R : Type u} [Semiring R] {p : Polynomial R} (h : p.Monic) {q : Polynomial R} :
(p * q).natDegree < p.natDegree p 1 q = 0
theorem Polynomial.Monic.mul_right_eq_zero_iff {R : Type u} [Semiring R] {p : Polynomial R} (h : p.Monic) {q : Polynomial R} :
p * q = 0 q = 0
theorem Polynomial.Monic.mul_left_eq_zero_iff {R : Type u} [Semiring R] {p : Polynomial R} (h : p.Monic) {q : Polynomial R} :
q * p = 0 q = 0
theorem Polynomial.Monic.isRegular {R : Type u_1} [Ring R] {p : Polynomial R} (hp : p.Monic) :
theorem Polynomial.degree_smul_of_smul_regular {R : Type u} [Semiring R] {S : Type u_1} [Monoid S] [DistribMulAction S R] {k : S} (p : Polynomial R) (h : IsSMulRegular R k) :
(k p).degree = p.degree
theorem Polynomial.natDegree_smul_of_smul_regular {R : Type u} [Semiring R] {S : Type u_1} [Monoid S] [DistribMulAction S R] {k : S} (p : Polynomial R) (h : IsSMulRegular R k) :
(k p).natDegree = p.natDegree
theorem Polynomial.leadingCoeff_smul_of_smul_regular {R : Type u} [Semiring R] {S : Type u_1} [Monoid S] [DistribMulAction S R] {k : S} (p : Polynomial R) (h : IsSMulRegular R k) :
(k p).leadingCoeff = k p.leadingCoeff
theorem Polynomial.monic_of_isUnit_leadingCoeff_inv_smul {R : Type u} [Semiring R] {p : Polynomial R} (h : IsUnit p.leadingCoeff) :
(h.unit⁻¹ p).Monic
theorem Polynomial.isUnit_leadingCoeff_mul_right_eq_zero_iff {R : Type u} [Semiring R] {p : Polynomial R} (h : IsUnit p.leadingCoeff) {q : Polynomial R} :
p * q = 0 q = 0
theorem Polynomial.isUnit_leadingCoeff_mul_left_eq_zero_iff {R : Type u} [Semiring R] {p : Polynomial R} (h : IsUnit p.leadingCoeff) {q : Polynomial R} :
q * p = 0 q = 0