Documentation

Mathlib.FieldTheory.Minpoly.MinpolyDiv

Results about minpoly R x / (X - C x) #

Main definition #

We used the contents of this file to describe the dual basis of a powerbasis under the trace form. See traceForm_dualBasis_powerBasis_eq.

Main results #

noncomputable def minpolyDiv (R : Type u_1) {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (x : S) :

minpolyDiv R x : S[X] for x : S is the polynomial minpoly R x / (X - C x).

Equations
Instances For
    theorem minpolyDiv_spec (R : Type u_2) {S : Type u_1} [CommRing R] [CommRing S] [Algebra R S] (x : S) :
    minpolyDiv R x * (Polynomial.X - Polynomial.C x) = Polynomial.map (algebraMap R S) (minpoly R x)
    theorem coeff_minpolyDiv (R : Type u_2) {S : Type u_1} [CommRing R] [CommRing S] [Algebra R S] (x : S) (i : ) :
    (minpolyDiv R x).coeff i = (algebraMap R S) ((minpoly R x).coeff (i + 1)) + (minpolyDiv R x).coeff (i + 1) * x
    theorem minpolyDiv_ne_zero {R : Type u_2} {S : Type u_1} [CommRing R] [CommRing S] [Algebra R S] {x : S} (hx : IsIntegral R x) [Nontrivial S] :
    theorem minpolyDiv_eq_zero {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {x : S} (hx : ¬IsIntegral R x) :
    theorem minpolyDiv_monic {R : Type u_2} {S : Type u_1} [CommRing R] [CommRing S] [Algebra R S] {x : S} (hx : IsIntegral R x) :
    (minpolyDiv R x).Monic
    theorem eval_minpolyDiv_self {R : Type u_2} {S : Type u_1} [CommRing R] [CommRing S] [Algebra R S] {x : S} :
    Polynomial.eval x (minpolyDiv R x) = (Polynomial.aeval x) (Polynomial.derivative (minpoly R x))
    theorem minpolyDiv_eval_eq_zero_of_ne_of_aeval_eq_zero {R : Type u_2} {S : Type u_1} [CommRing R] [CommRing S] [Algebra R S] {x : S} [IsDomain S] {y : S} (hxy : y x) (hy : (Polynomial.aeval y) (minpoly R x) = 0) :
    theorem eval₂_minpolyDiv_of_eval₂_eq_zero {R : Type u_3} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {T : Type u_1} [CommRing T] [IsDomain T] [DecidableEq T] {x : S} {y : T} (σ : S →+* T) (hy : Polynomial.eval₂ (σ.comp (algebraMap R S)) y (minpoly R x) = 0) :
    Polynomial.eval₂ σ y (minpolyDiv R x) = if σ x = y then σ ((Polynomial.aeval x) (Polynomial.derivative (minpoly R x))) else 0
    theorem eval₂_minpolyDiv_self {R : Type u_2} {S : Type u_3} [CommRing R] [CommRing S] [Algebra R S] {T : Type u_1} [CommRing T] [Algebra R T] [IsDomain T] [DecidableEq T] (x : S) (σ₁ : S →ₐ[R] T) (σ₂ : S →ₐ[R] T) :
    Polynomial.eval₂ (σ₁) (σ₂ x) (minpolyDiv R x) = if σ₁ x = σ₂ x then σ₁ ((Polynomial.aeval x) (Polynomial.derivative (minpoly R x))) else 0
    theorem eval_minpolyDiv_of_aeval_eq_zero {R : Type u_2} {S : Type u_1} [CommRing R] [CommRing S] [Algebra R S] {x : S} [IsDomain S] [DecidableEq S] {y : S} (hy : (Polynomial.aeval y) (minpoly R x) = 0) :
    Polynomial.eval y (minpolyDiv R x) = if x = y then (Polynomial.aeval x) (Polynomial.derivative (minpoly R x)) else 0
    theorem natDegree_minpolyDiv_succ {R : Type u_2} {S : Type u_1} [CommRing R] [CommRing S] [Algebra R S] {x : S} (hx : IsIntegral R x) [Nontrivial S] :
    (minpolyDiv R x).natDegree + 1 = (minpoly R x).natDegree
    theorem natDegree_minpolyDiv {R : Type u_2} {S : Type u_1} [CommRing R] [CommRing S] [Algebra R S] {x : S} :
    (minpolyDiv R x).natDegree = (minpoly R x).natDegree - 1
    theorem natDegree_minpolyDiv_lt {R : Type u_2} {S : Type u_1} [CommRing R] [CommRing S] [Algebra R S] {x : S} (hx : IsIntegral R x) [Nontrivial S] :
    (minpolyDiv R x).natDegree < (minpoly R x).natDegree
    theorem coeff_minpolyDiv_mem_adjoin {R : Type u_2} {S : Type u_1} [CommRing R] [CommRing S] [Algebra R S] (x : S) (i : ) :
    (minpolyDiv R x).coeff i Algebra.adjoin R {x}
    theorem minpolyDiv_eq_of_isIntegrallyClosed {R : Type u_1} (K : Type u_3) {S : Type u_2} [CommRing R] [Field K] [CommRing S] [Algebra R S] {x : S} (hx : IsIntegral R x) [IsDomain R] [IsIntegrallyClosed R] [IsDomain S] [Algebra R K] [Algebra K S] [IsScalarTower R K S] [IsFractionRing R K] :
    theorem coeff_minpolyDiv_sub_pow_mem_span {R : Type u_2} {S : Type u_1} [CommRing R] [CommRing S] [Algebra R S] {x : S} (hx : IsIntegral R x) {i : } (hi : i (minpolyDiv R x).natDegree) :
    (minpolyDiv R x).coeff ((minpolyDiv R x).natDegree - i) - x ^ i Submodule.span R ((fun (x_1 : ) => x ^ x_1) '' Set.Iio i)
    theorem span_coeff_minpolyDiv {R : Type u_2} {S : Type u_1} [CommRing R] [CommRing S] [Algebra R S] {x : S} (hx : IsIntegral R x) :
    Submodule.span R (Set.range (minpolyDiv R x).coeff) = Subalgebra.toSubmodule (Algebra.adjoin R {x})
    theorem sum_smul_minpolyDiv_eq_X_pow {K : Type u_2} {L : Type u_3} [Field K] [Field L] [Algebra K L] (E : Type u_1) [Field E] [Algebra K E] [IsAlgClosed E] [FiniteDimensional K L] [Algebra.IsSeparable K L] {x : L} (hxL : Algebra.adjoin K {x} = ) {r : } (hr : r < FiniteDimensional.finrank K L) :
    σ : L →ₐ[K] E, Polynomial.map (σ) ((x ^ r / (Polynomial.aeval x) (Polynomial.derivative (minpoly K x))) minpolyDiv K x) = Polynomial.X ^ r