data.polynomial.field_division

theorem polynomial.prod_multiset_root_eq_finset_root {R : Type u} [comm_ring R] [is_domain R] {p : R[X]} :

(multiset.map (λ (a : R), polynomial.X - ⇑polynomial.C a) p.roots).prod = ∏ (a : R) in p.roots.to_finset, (polynomial.X - ⇑polynomial.C a) ^ polynomial.root_multiplicity a p

source

theorem polynomial.roots_C_mul {R : Type u} [comm_ring R] [is_domain R] (p : R[X]) {a : R} (hzero : a ≠ 0) :

((⇑polynomial.C a) * p).roots = p.roots

source

theorem polynomial.derivative_root_multiplicity_of_root {R : Type u} [comm_ring R] [is_domain R] [char_zero R] {p : R[X]} {t : R} (hpt : p.is_root t) :

polynomial.root_multiplicity t (⇑polynomial.derivative p) = polynomial.root_multiplicity t p - 1

source

theorem polynomial.root_multiplicity_sub_one_le_derivative_root_multiplicity {R : Type u} [comm_ring R] [is_domain R] [char_zero R] (p : R[X]) (t : R) :

polynomial.root_multiplicity t p - 1 ≤ polynomial.root_multiplicity t (⇑polynomial.derivative p)

source

@[protected, instance]

noncomputable def polynomial.normalization_monoid {R : Type u} [comm_ring R] [is_domain R] [normalization_monoid R] :

normalization_monoid R[X]

Equations

polynomial.normalization_monoid = {norm_unit := λ (p : R[X]), {val := ⇑polynomial.C ↑(norm_unit p.leading_coeff), inv := ⇑polynomial.C ↑(norm_unit p.leading_coeff)⁻¹, val_inv := _, inv_val := _}, norm_unit_zero := _, norm_unit_mul := _, norm_unit_coe_units := _}

source

@[simp]

theorem polynomial.coe_norm_unit {R : Type u} [comm_ring R] [is_domain R] [normalization_monoid R] {p : R[X]} :

↑(norm_unit p) = ⇑polynomial.C ↑(norm_unit p.leading_coeff)

source

theorem polynomial.leading_coeff_normalize {R : Type u} [comm_ring R] [is_domain R] [normalization_monoid R] (p : R[X]) :

(⇑normalize p).leading_coeff = ⇑normalize p.leading_coeff

source

theorem polynomial.monic.normalize_eq_self {R : Type u} [comm_ring R] [is_domain R] [normalization_monoid R] {p : R[X]} (hp : p.monic) :

⇑normalize p = p

source

theorem polynomial.roots_normalize {R : Type u} [comm_ring R] [is_domain R] [normalization_monoid R] {p : R[X]} :

(⇑normalize p).roots = p.roots

source

theorem polynomial.degree_pos_of_ne_zero_of_nonunit {R : Type u} [division_ring R] {p : R[X]} (hp0 : p ≠ 0) (hp : ¬is_unit p) :

0 < p.degree

source

theorem polynomial.monic_mul_leading_coeff_inv {R : Type u} [division_ring R] {p : R[X]} (h : p ≠ 0) :

(p * ⇑polynomial.C (p.leading_coeff)⁻¹).monic

source

theorem polynomial.degree_mul_leading_coeff_inv {R : Type u} [division_ring R] {q : R[X]} (p : R[X]) (h : q ≠ 0) :

(p * ⇑polynomial.C (q.leading_coeff)⁻¹).degree = p.degree

source

@[simp]

theorem polynomial.map_eq_zero {R : Type u} {S : Type v} [division_ring R] {p : R[X]} [semiring S] [nontrivial S] (f : R →+* S) :

polynomial.map f p = 0 ↔ p = 0

source

theorem polynomial.map_ne_zero {R : Type u} {S : Type v} [division_ring R] {p : R[X]} [semiring S] [nontrivial S] {f : R →+* S} (hp : p ≠ 0) :

polynomial.map f p ≠ 0

source

theorem polynomial.is_unit_iff_degree_eq_zero {R : Type u} [field R] {p : R[X]} :

is_unit p ↔ p.degree = 0

source

theorem polynomial.irreducible_of_monic {R : Type u} [field R] {p : R[X]} (hp1 : p.monic) (hp2 : p ≠ 1) :

irreducible p ↔ ∀ (f g : R[X]), f.monic → g.monic → f * g = p → f = 1 ∨ g = 1

source

noncomputable def polynomial.div {R : Type u} [field R] (p q : R[X]) :

R[X]

Division of polynomials. See polynomial.div_by_monic for more details.

Equations

p.div q = (⇑polynomial.C (q.leading_coeff)⁻¹) * (p /ₘ q * ⇑polynomial.C (q.leading_coeff)⁻¹)

source

noncomputable def polynomial.mod {R : Type u} [field R] (p q : R[X]) :

R[X]

Remainder of polynomial division. See polynomial.mod_by_monic for more details.

Equations

p.mod q = p %ₘ q * ⇑polynomial.C (q.leading_coeff)⁻¹

source

@[protected, instance]

noncomputable def polynomial.has_div {R : Type u} [field R] :

has_div R[X]

Equations

polynomial.has_div = {div := polynomial.div _inst_1}

source

@[protected, instance]

noncomputable def polynomial.has_mod {R : Type u} [field R] :

has_mod R[X]

Equations

polynomial.has_mod = {mod := polynomial.mod _inst_1}

source

theorem polynomial.div_def {R : Type u} [field R] {p q : R[X]} :

p / q = (⇑polynomial.C (q.leading_coeff)⁻¹) * (p /ₘ q * ⇑polynomial.C (q.leading_coeff)⁻¹)

source

theorem polynomial.mod_def {R : Type u} [field R] {p q : R[X]} :

p % q = p %ₘ q * ⇑polynomial.C (q.leading_coeff)⁻¹

source

theorem polynomial.mod_by_monic_eq_mod {R : Type u} [field R] {q : R[X]} (p : R[X]) (hq : q.monic) :

p %ₘ q = p % q

source

theorem polynomial.div_by_monic_eq_div {R : Type u} [field R] {q : R[X]} (p : R[X]) (hq : q.monic) :

p /ₘ q = p / q

source

theorem polynomial.mod_X_sub_C_eq_C_eval {R : Type u} [field R] (p : R[X]) (a : R) :

p % (polynomial.X - ⇑polynomial.C a) = ⇑polynomial.C (polynomial.eval a p)

source

theorem polynomial.mul_div_eq_iff_is_root {R : Type u} {a : R} [field R] {p : R[X]} :

(polynomial.X - ⇑polynomial.C a) * (p / (polynomial.X - ⇑polynomial.C a)) = p ↔ p.is_root a

source

@[protected, instance]

noncomputable def polynomial.euclidean_domain {R : Type u} [field R] :

euclidean_domain R[X]

Equations

polynomial.euclidean_domain = {to_comm_ring := {add := comm_ring.add polynomial.comm_ring, add_assoc := _, zero := comm_ring.zero polynomial.comm_ring, zero_add := _, add_zero := _, nsmul := comm_ring.nsmul polynomial.comm_ring, nsmul_zero' := _, nsmul_succ' := _, neg := comm_ring.neg polynomial.comm_ring, sub := comm_ring.sub polynomial.comm_ring, sub_eq_add_neg := _, zsmul := comm_ring.zsmul polynomial.comm_ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := comm_ring.mul polynomial.comm_ring, mul_assoc := _, one := comm_ring.one polynomial.comm_ring, one_mul := _, mul_one := _, npow := comm_ring.npow polynomial.comm_ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _}, to_nontrivial := _, quotient := has_div.div polynomial.has_div, quotient_zero := _, remainder := has_mod.mod polynomial.has_mod, quotient_mul_add_remainder_eq := _, r := λ (p q : R[X]), p.degree < q.degree, r_well_founded := _, remainder_lt := _, mul_left_not_lt := _}

source

theorem polynomial.mod_eq_self_iff {R : Type u} [field R] {p q : R[X]} (hq0 : q ≠ 0) :

p % q = p ↔ p.degree < q.degree

source

theorem polynomial.div_eq_zero_iff {R : Type u} [field R] {p q : R[X]} (hq0 : q ≠ 0) :

p / q = 0 ↔ p.degree < q.degree

source

theorem polynomial.degree_add_div {R : Type u} [field R] {p q : R[X]} (hq0 : q ≠ 0) (hpq : q.degree ≤ p.degree) :

q.degree + (p / q).degree = p.degree

source

theorem polynomial.degree_div_le {R : Type u} [field R] (p q : R[X]) :

(p / q).degree ≤ p.degree

source

theorem polynomial.degree_div_lt {R : Type u} [field R] {p q : R[X]} (hp : p ≠ 0) (hq : 0 < q.degree) :

(p / q).degree < p.degree

source

@[simp]

theorem polynomial.degree_map {R : Type u} {k : Type y} [field R] [division_ring k] (p : R[X]) (f : R →+* k) :

(polynomial.map f p).degree = p.degree

source

@[simp]

theorem polynomial.nat_degree_map {R : Type u} {k : Type y} [field R] {p : R[X]} [division_ring k] (f : R →+* k) :

(polynomial.map f p).nat_degree = p.nat_degree

source

@[simp]

theorem polynomial.leading_coeff_map {R : Type u} {k : Type y} [field R] {p : R[X]} [division_ring k] (f : R →+* k) :

(polynomial.map f p).leading_coeff = ⇑f p.leading_coeff

source

theorem polynomial.monic_map_iff {R : Type u} {k : Type y} [field R] [division_ring k] {f : R →+* k} {p : R[X]} :

(polynomial.map f p).monic ↔ p.monic

source

theorem polynomial.is_unit_map {R : Type u} {k : Type y} [field R] {p : R[X]} [field k] (f : R →+* k) :

is_unit (polynomial.map f p) ↔ is_unit p

source

theorem polynomial.map_div {R : Type u} {k : Type y} [field R] {p q : R[X]} [field k] (f : R →+* k) :

polynomial.map f (p / q) = polynomial.map f p / polynomial.map f q

source

theorem polynomial.map_mod {R : Type u} {k : Type y} [field R] {p q : R[X]} [field k] (f : R →+* k) :

polynomial.map f (p % q) = polynomial.map f p % polynomial.map f q

source

theorem polynomial.gcd_map {R : Type u} {k : Type y} [field R] {p q : R[X]} [field k] (f : R →+* k) :

euclidean_domain.gcd (polynomial.map f p) (polynomial.map f q) = polynomial.map f (euclidean_domain.gcd p q)

source

theorem polynomial.eval₂_gcd_eq_zero {R : Type u} {k : Type y} [field R] [comm_semiring k] {ϕ : R →+* k} {f g : R[X]} {α : k} (hf : polynomial.eval₂ ϕ α f = 0) (hg : polynomial.eval₂ ϕ α g = 0) :

polynomial.eval₂ ϕ α (euclidean_domain.gcd f g) = 0

source

theorem polynomial.eval_gcd_eq_zero {R : Type u} [field R] {f g : R[X]} {α : R} (hf : polynomial.eval α f = 0) (hg : polynomial.eval α g = 0) :

polynomial.eval α (euclidean_domain.gcd f g) = 0

source

theorem polynomial.root_left_of_root_gcd {R : Type u} {k : Type y} [field R] [comm_semiring k] {ϕ : R →+* k} {f g : R[X]} {α : k} (hα : polynomial.eval₂ ϕ α (euclidean_domain.gcd f g) = 0) :

polynomial.eval₂ ϕ α f = 0

source

theorem polynomial.root_right_of_root_gcd {R : Type u} {k : Type y} [field R] [comm_semiring k] {ϕ : R →+* k} {f g : R[X]} {α : k} (hα : polynomial.eval₂ ϕ α (euclidean_domain.gcd f g) = 0) :

polynomial.eval₂ ϕ α g = 0

source

theorem polynomial.root_gcd_iff_root_left_right {R : Type u} {k : Type y} [field R] [comm_semiring k] {ϕ : R →+* k} {f g : R[X]} {α : k} :

polynomial.eval₂ ϕ α (euclidean_domain.gcd f g) = 0 ↔ polynomial.eval₂ ϕ α f = 0 ∧ polynomial.eval₂ ϕ α g = 0

source

theorem polynomial.is_root_gcd_iff_is_root_left_right {R : Type u} [field R] {f g : R[X]} {α : R} :

(euclidean_domain.gcd f g).is_root α ↔ f.is_root α ∧ g.is_root α

source

theorem polynomial.is_coprime_map {R : Type u} {k : Type y} [field R] {p q : R[X]} [field k] (f : R →+* k) :

is_coprime (polynomial.map f p) (polynomial.map f q) ↔ is_coprime p q

source

theorem polynomial.mem_roots_map {R : Type u} {k : Type y} [field R] {p : R[X]} [field k] {f : R →+* k} {x : k} (hp : p ≠ 0) :

x ∈ (polynomial.map f p).roots ↔ polynomial.eval₂ f x p = 0

source

theorem polynomial.mem_root_set {R : Type u} {k : Type y} [field R] {p : R[X]} [field k] [algebra R k] {x : k} (hp : p ≠ 0) :

x ∈ p.root_set k ↔ ⇑(polynomial.aeval x) p = 0

source

theorem polynomial.root_set_C_mul_X_pow {R : Type u_1} {S : Type u_2} [field R] [field S] [algebra R S] {n : ℕ} (hn : n ≠ 0) {a : R} (ha : a ≠ 0) :

((⇑polynomial.C a) * polynomial.X ^ n).root_set S = {0}

source

theorem polynomial.root_set_monomial {R : Type u_1} {S : Type u_2} [field R] [field S] [algebra R S] {n : ℕ} (hn : n ≠ 0) {a : R} (ha : a ≠ 0) :

(⇑(polynomial.monomial n) a).root_set S = {0}

source

theorem polynomial.root_set_X_pow {R : Type u_1} {S : Type u_2} [field R] [field S] [algebra R S] {n : ℕ} (hn : n ≠ 0) :

(polynomial.X ^ n).root_set S = {0}

source

theorem polynomial.exists_root_of_degree_eq_one {R : Type u} [field R] {p : R[X]} (h : p.degree = 1) :

∃ (x : R), p.is_root x

source

theorem polynomial.coeff_inv_units {R : Type u} [field R] (u : R[X]ˣ) (n : ℕ) :

(↑u.coeff n)⁻¹ = ↑u⁻¹.coeff n

source

theorem polynomial.monic_normalize {R : Type u} [field R] {p : R[X]} (hp0 : p ≠ 0) :

(⇑normalize p).monic

source

theorem polynomial.leading_coeff_div {R : Type u} [field R] {p q : R[X]} (hpq : q.degree ≤ p.degree) :

(p / q).leading_coeff = p.leading_coeff / q.leading_coeff

source

theorem polynomial.div_C_mul {R : Type u} {a : R} [field R] {p q : R[X]} :

p / (⇑polynomial.C a) * q = (⇑polynomial.C a⁻¹) * (p / q)

source

theorem polynomial.C_mul_dvd {R : Type u} {a : R} [field R] {p q : R[X]} (ha : a ≠ 0) :

(⇑polynomial.C a) * p ∣ q ↔ p ∣ q

source

theorem polynomial.dvd_C_mul {R : Type u} {a : R} [field R] {p q : R[X]} (ha : a ≠ 0) :

p ∣ (⇑polynomial.C a) * q ↔ p ∣ q

source

theorem polynomial.coe_norm_unit_of_ne_zero {R : Type u} [field R] {p : R[X]} (hp : p ≠ 0) :

↑(norm_unit p) = ⇑polynomial.C (p.leading_coeff)⁻¹

source

theorem polynomial.normalize_monic {R : Type u} [field R] {p : R[X]} (h : p.monic) :

⇑normalize p = p

source

theorem polynomial.map_dvd_map' {R : Type u} {k : Type y} [field R] [field k] (f : R →+* k) {x y : R[X]} :

polynomial.map f x ∣ polynomial.map f y ↔ x ∣ y

source

theorem polynomial.degree_normalize {R : Type u} [field R] {p : R[X]} :

(⇑normalize p).degree = p.degree

source

theorem polynomial.prime_of_degree_eq_one {R : Type u} [field R] {p : R[X]} (hp1 : p.degree = 1) :

prime p

source

theorem polynomial.irreducible_of_degree_eq_one {R : Type u} [field R] {p : R[X]} (hp1 : p.degree = 1) :

irreducible p

source

theorem polynomial.not_irreducible_C {R : Type u} [field R] (x : R) :

¬irreducible (⇑polynomial.C x)

source

theorem polynomial.degree_pos_of_irreducible {R : Type u} [field R] {p : R[X]} (hp : irreducible p) :

0 < p.degree

source

theorem polynomial.pairwise_coprime_X_sub {α : Type u} [field α] {I : Type v} {s : I → α} (H : function.injective s) :

pairwise (is_coprime on λ (i : I), polynomial.X - ⇑polynomial.C (s i))

source

theorem polynomial.is_coprime_of_is_root_of_eval_derivative_ne_zero {K : Type u_1} [field K] (f : K[X]) (a : K) (hf' : polynomial.eval a (⇑polynomial.derivative f) ≠ 0) :

is_coprime (polynomial.X - ⇑polynomial.C a) (f /ₘ (polynomial.X - ⇑polynomial.C a))

If f is a polynomial over a field, and a : K satisfies f' a ≠ 0, then f / (X - a) is coprime with X - a. Note that we do not assume f a = 0, because f / (X - a) = (f - f a) / (X - a).

source

theorem polynomial.prod_multiset_X_sub_C_dvd {R : Type u} [field R] (p : R[X]) :

(multiset.map (λ (a : R), polynomial.X - ⇑polynomial.C a) p.roots).prod ∣ p

The product ∏ (X - a) for a inside the multiset p.roots divides p.

mathlib documentation

Theory of univariate polynomials #