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, monic.pow.

theorem polynomial.monic.as_sum {R : Type u} [semiring R] {p : R[X]} (hp : p.monic) :
theorem polynomial.ne_zero_of_ne_zero_of_monic {R : Type u} [semiring R] {p q : R[X]} (hp : p 0) (hq : q.monic) :
q 0
theorem polynomial.monic.map {R : Type u} {S : Type v} [semiring R] {p : R[X]} [semiring S] (f : R →+* S) (hp : p.monic) :
theorem polynomial.monic_C_mul_of_mul_leading_coeff_eq_one {R : Type u} [semiring R] {p : R[X]} {b : R} (hp : b * p.leading_coeff = 1) :
theorem polynomial.monic_mul_C_of_leading_coeff_mul_eq_one {R : Type u} [semiring R] {p : R[X]} {b : R} (hp : (p.leading_coeff) * b = 1) :
theorem polynomial.monic_of_degree_le {R : Type u} [semiring R] {p : R[X]} (n : ) (H1 : p.degree n) (H2 : p.coeff n = 1) :
theorem polynomial.monic_X_pow_add {R : Type u} [semiring R] {p : R[X]} {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 : R[X]} (hp : p.monic) (hq : q.monic) :
(p * q).monic
theorem polynomial.monic.pow {R : Type u} [semiring R] {p : R[X]} (hp : p.monic) (n : ) :
(p ^ n).monic
theorem polynomial.monic.add_of_left {R : Type u} [semiring R] {p q : R[X]} (hp : p.monic) (hpq : q.degree < p.degree) :
(p + q).monic
theorem polynomial.monic.add_of_right {R : Type u} [semiring R] {p q : R[X]} (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 : R[X]} (hp : p.monic) (hpq : (p * q).monic) :
theorem polynomial.monic.of_mul_monic_right {R : Type u} [semiring R] {p q : R[X]} (hq : q.monic) (hpq : (p * q).monic) :
@[simp]
theorem polynomial.monic.nat_degree_eq_zero_iff_eq_one {R : Type u} [semiring R] {p : R[X]} (hp : p.monic) :
p.nat_degree = 0 p = 1
@[simp]
theorem polynomial.monic.degree_le_zero_iff_eq_one {R : Type u} [semiring R] {p : R[X]} (hp : p.monic) :
p.degree 0 p = 1
theorem polynomial.monic.nat_degree_mul {R : Type u} [semiring R] {p q : R[X]} (hp : p.monic) (hq : q.monic) :
theorem polynomial.monic.degree_mul_comm {R : Type u} [semiring R] {p : R[X]} (hp : p.monic) (q : R[X]) :
(p * q).degree = (q * p).degree
theorem polynomial.monic.nat_degree_mul' {R : Type u} [semiring R] {p q : R[X]} (hp : p.monic) (hq : q 0) :
theorem polynomial.monic.nat_degree_mul_comm {R : Type u} [semiring R] {p : R[X]} (hp : p.monic) (q : R[X]) :
(p * q).nat_degree = (q * p).nat_degree
theorem polynomial.monic.next_coeff_mul {R : Type u} [semiring R] {p q : R[X]} (hp : p.monic) (hq : q.monic) :
theorem polynomial.monic.eq_one_of_map_eq_one {R : Type u} [semiring R] {p : R[X]} {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.nat_degree_pow {R : Type u} [semiring R] {p : R[X]} (hp : p.monic) (n : ) :
@[simp]
theorem polynomial.nat_degree_pow_X_add_C {R : Type u} [semiring R] [nontrivial R] (n : ) (r : R) :
theorem polynomial.monic_multiset_prod_of_monic {R : Type u} {ι : Type y} [comm_semiring R] (t : multiset ι) (f : ι → R[X]) (ht : ∀ (i : ι), i t(f i).monic) :
theorem polynomial.monic_prod_of_monic {R : Type u} {ι : Type y} [comm_semiring R] (s : finset ι) (f : ι → R[X]) (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 : R[X]} (hm : p.monic) (hpu : is_unit p) :
p = 1
theorem polynomial.monic.next_coeff_multiset_prod {R : Type u} {ι : Type y} [comm_semiring R] (t : multiset ι) (f : ι → R[X]) (h : ∀ (i : ι), i t(f i).monic) :
(multiset.map f t).prod.next_coeff = (multiset.map (λ (i : ι), (f i).next_coeff) t).sum
theorem polynomial.monic.next_coeff_prod {R : Type u} {ι : Type y} [comm_semiring R] (s : finset ι) (f : ι → R[X]) (h : ∀ (i : ι), i s(f i).monic) :
(∏ (i : ι) in s, f i).next_coeff = ∑ (i : ι) in s, (f i).next_coeff
@[simp]
theorem polynomial.monic.nat_degree_map {R : Type u} {S : Type v} [semiring R] [semiring S] [nontrivial S] {P : R[X]} (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 : R[X]} (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 : R[X]) :
theorem polynomial.nat_degree_map_eq_of_injective {R : Type u} {S : Type v} [semiring R] [semiring S] {f : R →+* S} (hf : function.injective f) (p : R[X]) :
theorem polynomial.leading_coeff_map' {R : Type u} {S : Type v} [semiring R] [semiring S] {f : R →+* S} (hf : function.injective f) (p : R[X]) :
theorem polynomial.next_coeff_map {R : Type u} {S : Type v} [semiring R] [semiring S] {f : R →+* S} (hf : function.injective f) (p : R[X]) :
theorem polynomial.leading_coeff_of_injective {R : Type u} {S : Type v} [semiring R] [semiring S] {f : R →+* S} (hf : function.injective f) (p : R[X]) :
theorem polynomial.monic_of_injective {R : Type u} {S : Type v} [semiring R] [semiring S] {f : R →+* S} (hf : function.injective f) {p : R[X]} (hp : (polynomial.map f p).monic) :
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 : R[X]} {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 : R[X]} (hp : p.monic) (hpq : q.degree < p.degree) :
(p - q).monic
theorem polynomial.monic_sub_of_right {R : Type u} [ring R] {p q : R[X]} (hq : q.leading_coeff = -1) (hpq : p.degree < q.degree) :
(p - q).monic
@[simp]
theorem polynomial.not_monic_zero {R : Type u} [semiring R] [nontrivial R] :
theorem polynomial.monic.mul_left_ne_zero {R : Type u} [semiring R] {p : R[X]} (hp : p.monic) {q : R[X]} (hq : q 0) :
q * p 0
theorem polynomial.monic.mul_right_ne_zero {R : Type u} [semiring R] {p : R[X]} (hp : p.monic) {q : R[X]} (hq : q 0) :
p * q 0
theorem polynomial.monic.mul_nat_degree_lt_iff {R : Type u} [semiring R] {p : R[X]} (h : p.monic) {q : R[X]} :
(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 : R[X]} (h : p.monic) {q : R[X]} :
p * q = 0 q = 0
theorem polynomial.monic.mul_left_eq_zero_iff {R : Type u} [semiring R] {p : R[X]} (h : p.monic) {q : R[X]} :
q * p = 0 q = 0
theorem polynomial.monic.is_regular {R : Type u_1} [ring R] {p : R[X]} (hp : p.monic) :
theorem polynomial.degree_smul_of_smul_regular {R : Type u} [semiring R] {S : Type u_1} [monoid S] [distrib_mul_action S R] {k : S} (p : R[X]) (h : is_smul_regular R 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] [distrib_mul_action S R] {k : S} (p : R[X]) (h : is_smul_regular R k) :
theorem polynomial.leading_coeff_smul_of_smul_regular {R : Type u} [semiring R] {S : Type u_1} [monoid S] [distrib_mul_action S R] {k : S} (p : R[X]) (h : is_smul_regular R k) :
theorem polynomial.is_unit_leading_coeff_mul_right_eq_zero_iff {R : Type u} [semiring R] {p : R[X]} (h : is_unit p.leading_coeff) {q : R[X]} :
p * q = 0 q = 0
theorem polynomial.is_unit_leading_coeff_mul_left_eq_zero_iff {R : Type u} [semiring R] {p : R[X]} (h : is_unit p.leading_coeff) {q : R[X]} :
q * p = 0 q = 0