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.

source
theorem polynomial.monic.as_sum {R : Type u} [semiring R] {p : R[X]} (hp : p.monic) :
p = polynomial.X ^ p.nat_degree + ∑ (i : ℕ) in finset.range p.nat_degree, (⇑polynomial.C (p.coeff i)) * polynomial.X ^ i
source
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
source
theorem polynomial.monic.map {R : Type u} {S : Type v} [semiring R] {p : R[X]} [semiring S] (f : R →+* S) (hp : p.monic) :
(polynomial.map f p).monic
source
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) :
((⇑polynomial.C b) * p).monic
source
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) :
(p * ⇑polynomial.C b).monic
source
theorem polynomial.monic_of_degree_le {R : Type u} [semiring R] {p : R[X]} (n : ℕ) (H1 : p.degree ≤ ↑n) (H2 : p.coeff n = 1) :
p.monic
source
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
source
theorem polynomial.monic_X_add_C {R : Type u} [semiring R] (x : R) :
(polynomial.X + ⇑polynomial.C x).monic
source
theorem polynomial.monic.mul {R : Type u} [semiring R] {p q : R[X]} (hp : p.monic) (hq : q.monic) :
(p * q).monic
source
theorem polynomial.monic.pow {R : Type u} [semiring R] {p : R[X]} (hp : p.monic) (n : ℕ) :
(p ^ n).monic
source
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
source
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
source
theorem polynomial.monic.of_mul_monic_left {R : Type u} [semiring R] {p q : R[X]} (hp : p.monic) (hpq : (p * q).monic) :
q.monic
source
theorem polynomial.monic.of_mul_monic_right {R : Type u} [semiring R] {p q : R[X]} (hq : q.monic) (hpq : (p * q).monic) :
p.monic
source
@[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
source
@[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
source
theorem polynomial.monic.nat_degree_mul {R : Type u} [semiring R] {p q : R[X]} (hp : p.monic) (hq : q.monic) :
(p * q).nat_degree = p.nat_degree + q.nat_degree
source
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
source
theorem polynomial.monic.nat_degree_mul' {R : Type u} [semiring R] {p q : R[X]} (hp : p.monic) (hq : q ≠ 0) :
(p * q).nat_degree = p.nat_degree + q.nat_degree
source
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
source
theorem polynomial.monic.next_coeff_mul {R : Type u} [semiring R] {p q : R[X]} (hp : p.monic) (hq : q.monic) :
(p * q).next_coeff = p.next_coeff + q.next_coeff
source
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
source
theorem polynomial.monic.nat_degree_pow {R : Type u} [semiring R] {p : R[X]} (hp : p.monic) (n : ℕ) :
(p ^ n).nat_degree = n * p.nat_degree
source
@[simp]
theorem polynomial.nat_degree_pow_X_add_C {R : Type u} [semiring R] [nontrivial R] (n : ℕ) (r : R) :
((polynomial.X + ⇑polynomial.C r) ^ n).nat_degree = n
source
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) :
(multiset.map f t).prod.monic
source
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
source
theorem polynomial.is_unit_C {R : Type u} [comm_semiring R] {x : R} :
is_unit (⇑polynomial.C x) ↔ is_unit x
source
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
source
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
source
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
source
@[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) :
(polynomial.map f P).nat_degree = P.nat_degree
source
@[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) :
(polynomial.map f P).degree = P.degree
source
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]) :
(polynomial.map f p).degree = p.degree
source
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]) :
(polynomial.map f p).nat_degree = p.nat_degree
source
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]) :
(polynomial.map f p).leading_coeff = ⇑f p.leading_coeff
source
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]) :
(polynomial.map f p).next_coeff = ⇑f p.next_coeff
source
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]) :
(polynomial.map f p).leading_coeff = ⇑f p.leading_coeff
source
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) :
p.monic
source
theorem polynomial.monic_X_sub_C {R : Type u} [ring R] (x : R) :
(polynomial.X - ⇑polynomial.C x).monic
source
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
source
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.

source
theorem polynomial.not_is_unit_X_pow_sub_one (R : Type u_1) [comm_ring R] [nontrivial R] (n : ℕ) :
¬is_unit (polynomial.X ^ n - 1)
source
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
source
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
source
@[simp]
theorem polynomial.not_monic_zero {R : Type u} [semiring R] [nontrivial R] :
¬0.monic
source
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
source
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
source
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
source
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
source
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
source
theorem polynomial.monic.is_regular {R : Type u_1} [ring R] {p : R[X]} (hp : p.monic) :
is_regular p
source
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
source
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) :
(k • p).nat_degree = p.nat_degree
source
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) :
(k • p).leading_coeff = k • p.leading_coeff
source
theorem polynomial.monic_of_is_unit_leading_coeff_inv_smul {R : Type u} [semiring R] {p : R[X]} (h : is_unit p.leading_coeff) :
((h.unit)⁻¹ • p).monic
source
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
source
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