mathlib3documentation

data.polynomial.monic

Theory of monic polynomials #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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] :
0.monic ( (f g : , f = g) (a b : R), a = b
theorem polynomial.monic.as_sum {R : Type u} [semiring R] {p : polynomial R} (hp : p.monic) :
p = + (λ (i : ), polynomial.C (p.coeff i) *
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) :
p).monic
theorem polynomial.monic_C_mul_of_mul_leading_coeff_eq_one {R : Type u} [semiring R] {p : polynomial R} {b : R} (hp : = 1) :
* p).monic
theorem polynomial.monic_mul_C_of_leading_coeff_mul_eq_one {R : Type u} [semiring R] {p : polynomial R} {b : R} (hp : = 1) :
(p * .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) :
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
theorem polynomial.monic.of_mul_monic_left {R : Type u} [semiring R] {p q : polynomial R} (hp : p.monic) (hpq : (p * q).monic) :
theorem polynomial.monic.of_mul_monic_right {R : Type u} [semiring R] {p q : polynomial R} (hq : q.monic) (hpq : (p * q).monic) :
@[simp]
@[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.nat_degree_mul {R : Type u} [semiring R] {p q : polynomial R} (hp : p.monic) (hq : q.monic) :
(p * q).nat_degree =
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.nat_degree_mul' {R : Type u} [semiring R] {p q : polynomial R} (hp : p.monic) (hq : q 0) :
(p * q).nat_degree =
theorem polynomial.monic.nat_degree_mul_comm {R : Type u} [semiring R] {p : polynomial R} (hp : p.monic) (q : polynomial R) :
(p * q).nat_degree = (q * p).nat_degree
theorem polynomial.monic.not_dvd_of_nat_degree_lt {R : Type u} [semiring R] {p q : polynomial R} (hp : p.monic) (h0 : q 0) (hl : q.nat_degree < p.nat_degree) :
¬p q
theorem polynomial.monic.not_dvd_of_degree_lt {R : Type u} [semiring R] {p q : polynomial R} (hp : p.monic) (h0 : q 0) (hl : q.degree < p.degree) :
¬p q
theorem polynomial.monic.next_coeff_mul {R : Type u} [semiring R] {p q : polynomial R} (hp : p.monic) (hq : q.monic) :
(p * q).next_coeff =
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 : = 1) :
p = 1
theorem polynomial.monic.nat_degree_pow {R : Type u} [semiring R] {p : polynomial R} (hp : p.monic) (n : ) :
@[simp]
theorem polynomial.nat_degree_pow_X_add_C {R : Type u} [semiring R] [nontrivial R] (n : ) (r : R) :
^ n).nat_degree = n
theorem polynomial.monic.eq_one_of_is_unit {R : Type u} [semiring R] {p : polynomial R} (hm : p.monic) (hpu : is_unit p) :
p = 1
theorem polynomial.monic.is_unit_iff {R : Type u} [semiring R] {p : polynomial R} (hm : p.monic) :
p = 1
theorem polynomial.monic_multiset_prod_of_monic {R : Type u} {ι : Type y} (t : multiset ι) (f : ι ) (ht : (i : ι), i t (f i).monic) :
theorem polynomial.monic_prod_of_monic {R : Type u} {ι : Type y} (s : finset ι) (f : ι ) (hs : (i : ι), i s (f i).monic) :
(s.prod (λ (i : ι), f i)).monic
theorem polynomial.monic.next_coeff_multiset_prod {R : Type u} {ι : Type y} (t : multiset ι) (f : ι ) (h : (i : ι), i t (f i).monic) :
t).prod.next_coeff = (multiset.map (λ (i : ι), (f i).next_coeff) t).sum
theorem polynomial.monic.next_coeff_prod {R : Type u} {ι : Type y} (s : finset ι) (f : ι ) (h : (i : ι), i s (f i).monic) :
(s.prod (λ (i : ι), f i)).next_coeff = s.sum (λ (i : ι), (f i).next_coeff)
@[simp]
theorem polynomial.monic.nat_degree_map {R : Type u} {S : Type v} [semiring R] [semiring S] [nontrivial S] {P : polynomial R} (hmo : P.monic) (f : R →+* S) :
@[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) :
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) :
theorem polynomial.next_coeff_map {R : Type u} {S : Type v} [semiring R] [semiring S] {f : R →+* S} (hf : function.injective f) (p : polynomial R) :
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 : 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} :
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
@[simp]
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_nat_degree_lt_iff {R : Type u} [semiring R] {p : polynomial R} (h : p.monic) {q : polynomial R} :
(p * q).nat_degree < p.nat_degree 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.is_regular {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] [ R] {k : S} (p : polynomial R) (h : k) :
(k p).degree = p.degree
theorem polynomial.nat_degree_smul_of_smul_regular {R : Type u} [semiring R] {S : Type u_1} [monoid S] [ R] {k : S} (p : polynomial R) (h : k) :
theorem polynomial.leading_coeff_smul_of_smul_regular {R : Type u} [semiring R] {S : Type u_1} [monoid S] [ R] {k : S} (p : polynomial R) (h : k) :