Documentation

Mathlib.Algebra.Polynomial.Splits

Split polynomials #

A polynomial f : K[X] splits over a field extension L of K if it is zero or all of its irreducible factors over L have degree 1.

Main definitions #

def Polynomial.Splits {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) (f : Polynomial K) :

A polynomial Splits iff it is zero or all of its irreducible factors have degree 1.

Equations
Instances For
    @[simp]
    theorem Polynomial.splits_zero {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) :
    theorem Polynomial.splits_of_map_eq_C {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) {f : Polynomial K} {a : L} (h : Polynomial.map i f = Polynomial.C a) :
    @[simp]
    theorem Polynomial.splits_C {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) (a : K) :
    Polynomial.Splits i (Polynomial.C a)
    theorem Polynomial.splits_of_map_degree_eq_one {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) {f : Polynomial K} (hf : (Polynomial.map i f).degree = 1) :
    theorem Polynomial.splits_of_degree_le_one {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) {f : Polynomial K} (hf : f.degree 1) :
    theorem Polynomial.splits_of_degree_eq_one {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) {f : Polynomial K} (hf : f.degree = 1) :
    theorem Polynomial.splits_of_natDegree_le_one {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) {f : Polynomial K} (hf : f.natDegree 1) :
    theorem Polynomial.splits_of_natDegree_eq_one {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) {f : Polynomial K} (hf : f.natDegree = 1) :
    theorem Polynomial.splits_mul {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) {f g : Polynomial K} (hf : Polynomial.Splits i f) (hg : Polynomial.Splits i g) :
    theorem Polynomial.splits_of_splits_mul' {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) {f g : Polynomial K} (hfg : Polynomial.map i (f * g) 0) (h : Polynomial.Splits i (f * g)) :
    theorem Polynomial.splits_map_iff {F : Type u} {K : Type v} {L : Type w} [CommRing K] [Field L] [Field F] (i : K →+* L) (j : L →+* F) {f : Polynomial K} :
    theorem Polynomial.splits_one {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) :
    theorem Polynomial.splits_of_isUnit {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) [IsDomain K] {u : Polynomial K} (hu : IsUnit u) :
    theorem Polynomial.splits_X_sub_C {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) {x : K} :
    Polynomial.Splits i (Polynomial.X - Polynomial.C x)
    theorem Polynomial.splits_X {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) :
    Polynomial.Splits i Polynomial.X
    theorem Polynomial.splits_prod {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) {ι : Type u} {s : ιPolynomial K} {t : Finset ι} :
    (∀ jt, Polynomial.Splits i (s j))Polynomial.Splits i (∏ xt, s x)
    theorem Polynomial.splits_pow {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) {f : Polynomial K} (hf : Polynomial.Splits i f) (n : ) :
    theorem Polynomial.splits_X_pow {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) (n : ) :
    Polynomial.Splits i (Polynomial.X ^ n)
    theorem Polynomial.Splits.comp_of_map_degree_le_one {K : Type v} {L : Type w} [CommRing K] [Field L] {i : K →+* L} {f p : Polynomial K} (hd : (Polynomial.map i p).degree 1) (h : Polynomial.Splits i f) :
    Polynomial.Splits i (f.comp p)
    theorem Polynomial.splits_iff_comp_splits_of_degree_eq_one {K : Type v} {L : Type w} [CommRing K] [Field L] {i : K →+* L} {f p : Polynomial K} (hd : (Polynomial.map i p).degree = 1) :
    theorem Polynomial.Splits.comp_of_degree_le_one {K : Type v} {L : Type w} [CommRing K] [Field L] {i : K →+* L} {f p : Polynomial K} (hd : p.degree 1) (h : Polynomial.Splits i f) :
    Polynomial.Splits i (f.comp p)

    This is a weaker variant of Splits.comp_of_map_degree_le_one, but its conditions are easier to check.

    theorem Polynomial.Splits.comp_X_sub_C {K : Type v} {L : Type w} [CommRing K] [Field L] {i : K →+* L} (a : K) {f : Polynomial K} (h : Polynomial.Splits i f) :
    Polynomial.Splits i (f.comp (Polynomial.X - Polynomial.C a))
    theorem Polynomial.Splits.comp_X_add_C {K : Type v} {L : Type w} [CommRing K] [Field L] {i : K →+* L} (a : K) {f : Polynomial K} (h : Polynomial.Splits i f) :
    Polynomial.Splits i (f.comp (Polynomial.X + Polynomial.C a))
    theorem Polynomial.Splits.comp_neg_X {K : Type v} {L : Type w} [CommRing K] [Field L] {i : K →+* L} {f : Polynomial K} (h : Polynomial.Splits i f) :
    Polynomial.Splits i (f.comp (-Polynomial.X))
    theorem Polynomial.exists_root_of_splits' {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) {f : Polynomial K} (hs : Polynomial.Splits i f) (hf0 : (Polynomial.map i f).degree 0) :
    ∃ (x : L), Polynomial.eval₂ i x f = 0
    theorem Polynomial.roots_ne_zero_of_splits' {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) {f : Polynomial K} (hs : Polynomial.Splits i f) (hf0 : (Polynomial.map i f).natDegree 0) :
    (Polynomial.map i f).roots 0
    def Polynomial.rootOfSplits' {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) {f : Polynomial K} (hf : Polynomial.Splits i f) (hfd : (Polynomial.map i f).degree 0) :
    L

    Pick a root of a polynomial that splits. See rootOfSplits for polynomials over a field which has simpler assumptions.

    Equations
    Instances For
      theorem Polynomial.map_rootOfSplits' {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) {f : Polynomial K} (hf : Polynomial.Splits i f) (hfd : (Polynomial.map i f).degree 0) :
      theorem Polynomial.natDegree_eq_card_roots' {K : Type v} {L : Type w} [CommRing K] [Field L] {p : Polynomial K} {i : K →+* L} (hsplit : Polynomial.Splits i p) :
      (Polynomial.map i p).natDegree = Multiset.card (Polynomial.map i p).roots
      theorem Polynomial.degree_eq_card_roots' {K : Type v} {L : Type w} [CommRing K] [Field L] {p : Polynomial K} {i : K →+* L} (p_ne_zero : Polynomial.map i p 0) (hsplit : Polynomial.Splits i p) :
      (Polynomial.map i p).degree = (Multiset.card (Polynomial.map i p).roots)
      theorem Polynomial.splits_iff {K : Type v} {L : Type w} [Field K] [Field L] (i : K →+* L) (f : Polynomial K) :
      Polynomial.Splits i f f = 0 ∀ {g : Polynomial L}, Irreducible gg Polynomial.map i fg.degree = 1

      This lemma is for polynomials over a field.

      theorem Polynomial.Splits.def {K : Type v} {L : Type w} [Field K] [Field L] {i : K →+* L} {f : Polynomial K} (h : Polynomial.Splits i f) :
      f = 0 ∀ {g : Polynomial L}, Irreducible gg Polynomial.map i fg.degree = 1

      This lemma is for polynomials over a field.

      theorem Polynomial.splits_of_splits_mul {K : Type v} {L : Type w} [Field K] [Field L] (i : K →+* L) {f g : Polynomial K} (hfg : f * g 0) (h : Polynomial.Splits i (f * g)) :
      theorem Polynomial.splits_of_splits_of_dvd {K : Type v} {L : Type w} [Field K] [Field L] (i : K →+* L) {f g : Polynomial K} (hf0 : f 0) (hf : Polynomial.Splits i f) (hgf : g f) :
      theorem Polynomial.splits_of_splits_gcd_left {K : Type v} {L : Type w} [Field K] [Field L] (i : K →+* L) [DecidableEq K] {f g : Polynomial K} (hf0 : f 0) (hf : Polynomial.Splits i f) :
      theorem Polynomial.splits_of_splits_gcd_right {K : Type v} {L : Type w} [Field K] [Field L] (i : K →+* L) [DecidableEq K] {f g : Polynomial K} (hg0 : g 0) (hg : Polynomial.Splits i g) :
      theorem Polynomial.splits_mul_iff {K : Type v} {L : Type w} [Field K] [Field L] (i : K →+* L) {f g : Polynomial K} (hf : f 0) (hg : g 0) :
      theorem Polynomial.splits_prod_iff {K : Type v} {L : Type w} [Field K] [Field L] (i : K →+* L) {ι : Type u} {s : ιPolynomial K} {t : Finset ι} :
      (∀ jt, s j 0)(Polynomial.Splits i (∏ xt, s x) jt, Polynomial.Splits i (s j))
      theorem Polynomial.degree_eq_one_of_irreducible_of_splits {K : Type v} [Field K] {p : Polynomial K} (hp : Irreducible p) (hp_splits : Polynomial.Splits (RingHom.id K) p) :
      p.degree = 1
      theorem Polynomial.exists_root_of_splits {K : Type v} {L : Type w} [Field K] [Field L] (i : K →+* L) {f : Polynomial K} (hs : Polynomial.Splits i f) (hf0 : f.degree 0) :
      ∃ (x : L), Polynomial.eval₂ i x f = 0
      theorem Polynomial.roots_ne_zero_of_splits {K : Type v} {L : Type w} [Field K] [Field L] (i : K →+* L) {f : Polynomial K} (hs : Polynomial.Splits i f) (hf0 : f.natDegree 0) :
      (Polynomial.map i f).roots 0
      def Polynomial.rootOfSplits {K : Type v} {L : Type w} [Field K] [Field L] (i : K →+* L) {f : Polynomial K} (hf : Polynomial.Splits i f) (hfd : f.degree 0) :
      L

      Pick a root of a polynomial that splits. This version is for polynomials over a field and has simpler assumptions.

      Equations
      Instances For
        theorem Polynomial.rootOfSplits'_eq_rootOfSplits {K : Type v} {L : Type w} [Field K] [Field L] (i : K →+* L) {f : Polynomial K} (hf : Polynomial.Splits i f) (hfd : (Polynomial.map i f).degree 0) :

        rootOfSplits' is definitionally equal to rootOfSplits.

        theorem Polynomial.map_rootOfSplits {K : Type v} {L : Type w} [Field K] [Field L] (i : K →+* L) {f : Polynomial K} (hf : Polynomial.Splits i f) (hfd : f.degree 0) :
        theorem Polynomial.natDegree_eq_card_roots {K : Type v} {L : Type w} [Field K] [Field L] {p : Polynomial K} {i : K →+* L} (hsplit : Polynomial.Splits i p) :
        p.natDegree = Multiset.card (Polynomial.map i p).roots
        theorem Polynomial.degree_eq_card_roots {K : Type v} {L : Type w} [Field K] [Field L] {p : Polynomial K} {i : K →+* L} (p_ne_zero : p 0) (hsplit : Polynomial.Splits i p) :
        p.degree = (Multiset.card (Polynomial.map i p).roots)
        theorem Polynomial.roots_map {K : Type v} {L : Type w} [Field K] [Field L] (i : K →+* L) {f : Polynomial K} (hf : Polynomial.Splits (RingHom.id K) f) :
        (Polynomial.map i f).roots = Multiset.map (⇑i) f.roots
        theorem Polynomial.image_rootSet {R : Type u_1} {K : Type v} {L : Type w} [CommRing R] [Field K] [Field L] [Algebra R K] [Algebra R L] {p : Polynomial R} (h : Polynomial.Splits (algebraMap R K) p) (f : K →ₐ[R] L) :
        f '' p.rootSet K = p.rootSet L
        theorem Polynomial.adjoin_rootSet_eq_range {R : Type u_1} {K : Type v} {L : Type w} [CommRing R] [Field K] [Field L] [Algebra R K] [Algebra R L] {p : Polynomial R} (h : Polynomial.Splits (algebraMap R K) p) (f : K →ₐ[R] L) :
        Algebra.adjoin R (p.rootSet L) = f.range Algebra.adjoin R (p.rootSet K) =
        theorem Polynomial.eq_prod_roots_of_splits {K : Type v} {L : Type w} [Field K] [Field L] {p : Polynomial K} {i : K →+* L} (hsplit : Polynomial.Splits i p) :
        Polynomial.map i p = Polynomial.C (i p.leadingCoeff) * (Multiset.map (fun (a : L) => Polynomial.X - Polynomial.C a) (Polynomial.map i p).roots).prod
        theorem Polynomial.eq_prod_roots_of_splits_id {K : Type v} [Field K] {p : Polynomial K} (hsplit : Polynomial.Splits (RingHom.id K) p) :
        p = Polynomial.C p.leadingCoeff * (Multiset.map (fun (a : K) => Polynomial.X - Polynomial.C a) p.roots).prod
        theorem Polynomial.Splits.dvd_of_roots_le_roots {K : Type v} [Field K] {p q : Polynomial K} (hp : Polynomial.Splits (RingHom.id K) p) (hp0 : p 0) (hq : p.roots q.roots) :
        p q
        theorem Polynomial.Splits.dvd_iff_roots_le_roots {K : Type v} [Field K] {p q : Polynomial K} (hp : Polynomial.Splits (RingHom.id K) p) (hp0 : p 0) (hq0 : q 0) :
        p q p.roots q.roots
        theorem Polynomial.aeval_eq_prod_aroots_sub_of_splits {K : Type v} {L : Type w} [Field K] [Field L] [Algebra K L] {p : Polynomial K} (hsplit : Polynomial.Splits (algebraMap K L) p) (v : L) :
        (Polynomial.aeval v) p = (algebraMap K L) p.leadingCoeff * (Multiset.map (fun (a : L) => v - a) (p.aroots L)).prod
        theorem Polynomial.eval_eq_prod_roots_sub_of_splits_id {K : Type v} [Field K] {p : Polynomial K} (hsplit : Polynomial.Splits (RingHom.id K) p) (v : K) :
        Polynomial.eval v p = p.leadingCoeff * (Multiset.map (fun (a : K) => v - a) p.roots).prod
        theorem Polynomial.eq_prod_roots_of_monic_of_splits_id {K : Type v} [Field K] {p : Polynomial K} (m : p.Monic) (hsplit : Polynomial.Splits (RingHom.id K) p) :
        p = (Multiset.map (fun (a : K) => Polynomial.X - Polynomial.C a) p.roots).prod
        theorem Polynomial.aeval_eq_prod_aroots_sub_of_monic_of_splits {K : Type v} {L : Type w} [Field K] [Field L] [Algebra K L] {p : Polynomial K} (m : p.Monic) (hsplit : Polynomial.Splits (algebraMap K L) p) (v : L) :
        (Polynomial.aeval v) p = (Multiset.map (fun (a : L) => v - a) (p.aroots L)).prod
        theorem Polynomial.eval_eq_prod_roots_sub_of_monic_of_splits_id {K : Type v} [Field K] {p : Polynomial K} (m : p.Monic) (hsplit : Polynomial.Splits (RingHom.id K) p) (v : K) :
        Polynomial.eval v p = (Multiset.map (fun (a : K) => v - a) p.roots).prod
        theorem Polynomial.eq_X_sub_C_of_splits_of_single_root {K : Type v} {L : Type w} [Field K] [Field L] (i : K →+* L) {x : K} {h : Polynomial K} (h_splits : Polynomial.Splits i h) (h_roots : (Polynomial.map i h).roots = {i x}) :
        h = Polynomial.C h.leadingCoeff * (Polynomial.X - Polynomial.C x)
        theorem Polynomial.mem_lift_of_splits_of_roots_mem_range (R : Type u_1) {K : Type v} [CommRing R] [Field K] [Algebra R K] {f : Polynomial K} (hs : Polynomial.Splits (RingHom.id K) f) (hm : f.Monic) (hr : af.roots, a (algebraMap R K).range) :
        theorem Polynomial.splits_of_exists_multiset {K : Type v} {L : Type w} [Field K] [Field L] (i : K →+* L) {f : Polynomial K} {s : Multiset L} (hs : Polynomial.map i f = Polynomial.C (i f.leadingCoeff) * (Multiset.map (fun (a : L) => Polynomial.X - Polynomial.C a) s).prod) :
        theorem Polynomial.splits_iff_exists_multiset {K : Type v} {L : Type w} [Field K] [Field L] (i : K →+* L) {f : Polynomial K} :
        Polynomial.Splits i f ∃ (s : Multiset L), Polynomial.map i f = Polynomial.C (i f.leadingCoeff) * (Multiset.map (fun (a : L) => Polynomial.X - Polynomial.C a) s).prod
        theorem Polynomial.splits_of_comp {F : Type u} {K : Type v} {L : Type w} [Field K] [Field L] [Field F] (i : K →+* L) (j : L →+* F) {f : Polynomial K} (h : Polynomial.Splits (j.comp i) f) (roots_mem_range : a(Polynomial.map (j.comp i) f).roots, a j.range) :
        theorem Polynomial.splits_id_of_splits {K : Type v} {L : Type w} [Field K] [Field L] (i : K →+* L) {f : Polynomial K} (h : Polynomial.Splits i f) (roots_mem_range : a(Polynomial.map i f).roots, a i.range) :
        theorem Polynomial.splits_comp_of_splits {R : Type u_1} {K : Type v} {L : Type w} [CommRing R] [Field K] [Field L] (i : R →+* K) (j : K →+* L) {f : Polynomial R} (h : Polynomial.Splits i f) :
        Polynomial.Splits (j.comp i) f
        theorem Polynomial.splits_of_algHom {R : Type u_1} {K : Type v} {L : Type w} [CommRing R] [Field K] [Field L] [Algebra R K] [Algebra R L] {f : Polynomial R} (h : Polynomial.Splits (algebraMap R K) f) (e : K →ₐ[R] L) :
        theorem Polynomial.splits_of_isScalarTower {R : Type u_1} {K : Type v} (L : Type w) [CommRing R] [Field K] [Field L] [Algebra R K] [Algebra R L] {f : Polynomial R} [Algebra K L] [IsScalarTower R K L] (h : Polynomial.Splits (algebraMap R K) f) :
        theorem Polynomial.splits_iff_card_roots {K : Type v} [Field K] {p : Polynomial K} :
        Polynomial.Splits (RingHom.id K) p Multiset.card p.roots = p.natDegree

        A polynomial splits if and only if it has as many roots as its degree.

        theorem Polynomial.aeval_root_derivative_of_splits {K : Type v} {L : Type w} [Field K] [Field L] [Algebra K L] [DecidableEq L] {P : Polynomial K} (hmo : P.Monic) (hP : Polynomial.Splits (algebraMap K L) P) {r : L} (hr : r P.aroots L) :
        (Polynomial.aeval r) (Polynomial.derivative P) = (Multiset.map (fun (a : L) => r - a) ((P.aroots L).erase r)).prod
        theorem Polynomial.prod_roots_eq_coeff_zero_of_monic_of_splits {K : Type v} [Field K] {P : Polynomial K} (hmo : P.Monic) (hP : Polynomial.Splits (RingHom.id K) P) :
        P.coeff 0 = (-1) ^ P.natDegree * P.roots.prod

        If P is a monic polynomial that splits, then coeff P 0 equals the product of the roots.

        @[deprecated Polynomial.prod_roots_eq_coeff_zero_of_monic_of_splits]
        theorem Polynomial.prod_roots_eq_coeff_zero_of_monic_of_split {K : Type v} [Field K] {P : Polynomial K} (hmo : P.Monic) (hP : Polynomial.Splits (RingHom.id K) P) :
        P.coeff 0 = (-1) ^ P.natDegree * P.roots.prod

        Alias of Polynomial.prod_roots_eq_coeff_zero_of_monic_of_splits.


        If P is a monic polynomial that splits, then coeff P 0 equals the product of the roots.

        theorem Polynomial.sum_roots_eq_nextCoeff_of_monic_of_split {K : Type v} [Field K] {P : Polynomial K} (hmo : P.Monic) (hP : Polynomial.Splits (RingHom.id K) P) :
        P.nextCoeff = -P.roots.sum

        If P is a monic polynomial that splits, then P.nextCoeff equals the sum of the roots.