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

## Main definition #

• minpolyDiv: The polynomial minpoly R x / (X - C x).

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 #

• span_coeff_minpolyDiv: The coefficients of minpolyDiv spans R<x>.
noncomputable def minpolyDiv (R : Type u_1) {S : Type u_2} [] [] [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} [] [] [Algebra R S] (x : S) :
* (Polynomial.X - Polynomial.C x) = Polynomial.map () (minpoly R x)
theorem coeff_minpolyDiv (R : Type u_2) {S : Type u_1} [] [] [Algebra R S] (x : S) (i : ) :
().coeff i = () ((minpoly R x).coeff (i + 1)) + ().coeff (i + 1) * x
theorem minpolyDiv_ne_zero {R : Type u_2} {S : Type u_1} [] [] [Algebra R S] {x : S} (hx : ) [] :
0
theorem minpolyDiv_eq_zero {R : Type u_2} {S : Type u_1} [] [] [Algebra R S] {x : S} (hx : ¬) :
= 0
theorem minpolyDiv_monic {R : Type u_2} {S : Type u_1} [] [] [Algebra R S] {x : S} (hx : ) :
().Monic
theorem eval_minpolyDiv_self {R : Type u_2} {S : Type u_1} [] [] [Algebra R S] {x : S} :
Polynomial.eval 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} [] [] [Algebra R S] {x : S} [] {y : S} (hxy : y x) (hy : () (minpoly R x) = 0) :
theorem eval₂_minpolyDiv_of_eval₂_eq_zero {R : Type u_3} {S : Type u_2} [] [] [Algebra R S] {T : Type u_1} [] [] [] {x : S} {y : T} (σ : S →+* T) (hy : Polynomial.eval₂ (σ.comp ()) y (minpoly R x) = 0) :
Polynomial.eval₂ σ y () = if σ x = y then σ (() (Polynomial.derivative (minpoly R x))) else 0
theorem eval₂_minpolyDiv_self {R : Type u_2} {S : Type u_3} [] [] [Algebra R S] {T : Type u_1} [] [Algebra R T] [] [] (x : S) (σ₁ : S →ₐ[R] T) (σ₂ : S →ₐ[R] T) :
Polynomial.eval₂ (σ₁) (σ₂ x) () = if σ₁ x = σ₂ x then σ₁ (() (Polynomial.derivative (minpoly R x))) else 0
theorem eval_minpolyDiv_of_aeval_eq_zero {R : Type u_2} {S : Type u_1} [] [] [Algebra R S] {x : S} [] [] {y : S} (hy : () (minpoly R x) = 0) :
Polynomial.eval y () = if x = y then () (Polynomial.derivative (minpoly R x)) else 0
theorem natDegree_minpolyDiv_succ {R : Type u_2} {S : Type u_1} [] [] [Algebra R S] {x : S} (hx : ) [] :
().natDegree + 1 = (minpoly R x).natDegree
theorem natDegree_minpolyDiv {R : Type u_2} {S : Type u_1} [] [] [Algebra R S] {x : S} :
().natDegree = (minpoly R x).natDegree - 1
theorem natDegree_minpolyDiv_lt {R : Type u_2} {S : Type u_1} [] [] [Algebra R S] {x : S} (hx : ) [] :
().natDegree < (minpoly R x).natDegree
theorem coeff_minpolyDiv_mem_adjoin {R : Type u_2} {S : Type u_1} [] [] [Algebra R S] (x : S) (i : ) :