# Minimal polynomials on an algebra over a field #

This file specializes the theory of minpoly to the setting of field extensions and derives some well-known properties, amongst which the fact that minimal polynomials are irreducible, and uniquely determined by their defining property.

theorem minpoly.degree_le_of_ne_zero (A : Type u_1) {B : Type u_2} [] [Ring B] [Algebra A B] (x : B) {p : } (pnz : p 0) (hp : () p = 0) :
(minpoly A x).degree p.degree

If an element x is a root of a nonzero polynomial p, then the degree of p is at least the degree of the minimal polynomial of x. See also minpoly.IsIntegrallyClosed.degree_le_of_ne_zero which relaxes the assumptions on A in exchange for stronger assumptions on B.

theorem minpoly.ne_zero_of_finite (A : Type u_1) {B : Type u_2} [] [Ring B] [Algebra A B] (e : B) [] :
minpoly A e 0
theorem minpoly.unique (A : Type u_1) {B : Type u_2} [] [Ring B] [Algebra A B] (x : B) {p : } (pmonic : p.Monic) (hp : () p = 0) (pmin : ∀ (q : ), q.Monic() q = 0p.degree q.degree) :
p = minpoly A x

The minimal polynomial of an element x is uniquely characterized by its defining property: if there is another monic polynomial of minimal degree that has x as a root, then this polynomial is equal to the minimal polynomial of x. See also minpoly.IsIntegrallyClosed.Minpoly.unique which relaxes the assumptions on A in exchange for stronger assumptions on B.

theorem minpoly.dvd (A : Type u_1) {B : Type u_2} [] [Ring B] [Algebra A B] (x : B) {p : } (hp : () p = 0) :
minpoly A x p

If an element x is a root of a polynomial p, then the minimal polynomial of x divides p. See also minpoly.isIntegrallyClosed_dvd which relaxes the assumptions on A in exchange for stronger assumptions on B.

theorem minpoly.dvd_iff {A : Type u_1} {B : Type u_2} [] [Ring B] [Algebra A B] {x : B} {p : } :
minpoly A x p () p = 0
theorem minpoly.isRadical (A : Type u_1) {B : Type u_2} [] [Ring B] [Algebra A B] (x : B) [] :
theorem minpoly.dvd_map_of_isScalarTower (A : Type u_3) (K : Type u_4) {R : Type u_5} [] [] [] [Algebra A K] [Algebra A R] [Algebra K R] [] (x : R) :
theorem minpoly.dvd_map_of_isScalarTower' (R : Type u_3) {S : Type u_4} (K : Type u_5) (L : Type u_6) [] [] [] [] [Algebra R S] [Algebra R K] [Algebra S L] [Algebra K L] [Algebra R L] [] [] (s : S) :
minpoly K (() s) Polynomial.map () (minpoly R s)
theorem minpoly.aeval_of_isScalarTower (R : Type u_3) {K : Type u_4} {T : Type u_5} {U : Type u_6} [] [] [] [Algebra R K] [Algebra K T] [Algebra R T] [] [] [Algebra K U] [Algebra R U] [] (x : T) (y : U) (hy : () (minpoly K x) = 0) :
() (minpoly R x) = 0

If y is a conjugate of x over a field K, then it is a conjugate over a subring R.

@[simp]
theorem minpoly.ker_aeval_eq_span_minpoly (A : Type u_1) {B : Type u_2} [] [Ring B] [Algebra A B] (x : B) :

See also minpoly.ker_eval which relaxes the assumptions on A in exchange for stronger assumptions on B.

theorem minpoly.eq_of_irreducible_of_monic {A : Type u_1} {B : Type u_2} [] [Ring B] [Algebra A B] {x : B} [] {p : } (hp1 : ) (hp2 : () p = 0) (hp3 : p.Monic) :
p = minpoly A x
theorem minpoly.eq_of_irreducible {A : Type u_1} {B : Type u_2} [] [Ring B] [Algebra A B] {x : B} [] {p : } (hp1 : ) (hp2 : () p = 0) :
p * Polynomial.C p.leadingCoeff⁻¹ = minpoly A x
theorem minpoly.add_algebraMap {A : Type u_1} [] {B : Type u_3} [] [Algebra A B] {x : B} (hx : ) (a : A) :
minpoly A (x + () a) = (minpoly A x).comp (Polynomial.X - Polynomial.C a)
theorem minpoly.sub_algebraMap {A : Type u_1} [] {B : Type u_3} [] [Algebra A B] {x : B} (hx : ) (a : A) :
minpoly A (x - () a) = (minpoly A x).comp (Polynomial.X + Polynomial.C a)
noncomputable def minpoly.Fintype.subtypeProd {E : Type u_3} {X : Set E} (hX : X.Finite) {L : Type u_4} (F : E) :
Fintype ((x : X) → { l : L // l F x })

A technical finiteness result.

Equations
• = Pi.fintype
Instances For
def minpoly.rootsOfMinPolyPiType (F : Type u_3) (E : Type u_4) (K : Type u_5) [] [Ring E] [] [] [Algebra F E] [Algebra F K] [] (φ : E →ₐ[F] K) (x : ()) :
{ l : K // l (minpoly F x).aroots K }

Function from Hom_K(E,L) to pi type Π (x : basis), roots of min poly of x

Equations
• = φ x,
Instances For
theorem minpoly.aux_inj_roots_of_min_poly (F : Type u_3) (E : Type u_4) (K : Type u_5) [] [Ring E] [] [] [Algebra F E] [Algebra F K] [] :
noncomputable instance minpoly.AlgHom.fintype (F : Type u_3) (E : Type u_4) (K : Type u_5) [] [Ring E] [] [] [Algebra F E] [Algebra F K] [] :

Given field extensions E/F and K/F, with E/F finite, there are finitely many F-algebra homomorphisms E →ₐ[K] K.

Equations
theorem minpoly.eq_X_sub_C {A : Type u_1} (B : Type u_2) [] [Ring B] [Algebra A B] [] (a : A) :
minpoly A (() a) = Polynomial.X - Polynomial.C a

If B/K is a nontrivial algebra over a field, and x is an element of K, then the minimal polynomial of algebraMap K B x is X - C x.

theorem minpoly.eq_X_sub_C' {A : Type u_1} [] (a : A) :
minpoly A a = Polynomial.X - Polynomial.C a
@[simp]
theorem minpoly.zero (A : Type u_1) (B : Type u_2) [] [Ring B] [Algebra A B] [] :
minpoly A 0 = Polynomial.X

The minimal polynomial of 0 is X.

@[simp]
theorem minpoly.one (A : Type u_1) (B : Type u_2) [] [Ring B] [Algebra A B] [] :
minpoly A 1 = Polynomial.X - 1

The minimal polynomial of 1 is X - 1.

theorem minpoly.prime {A : Type u_1} {B : Type u_2} [] [Ring B] [] [Algebra A B] {x : B} (hx : ) :

A minimal polynomial is prime.

theorem minpoly.root {A : Type u_1} {B : Type u_2} [] [Ring B] [] [Algebra A B] {x : B} (hx : ) {y : A} (h : (minpoly A x).IsRoot y) :
() y = x

If L/K is a field extension and an element y of K is a root of the minimal polynomial of an element x ∈ L, then y maps to x under the field embedding.

@[simp]
theorem minpoly.coeff_zero_eq_zero {A : Type u_1} {B : Type u_2} [] [Ring B] [] [Algebra A B] {x : B} (hx : ) :
(minpoly A x).coeff 0 = 0 x = 0

The constant coefficient of the minimal polynomial of x is 0 if and only if x = 0.

theorem minpoly.coeff_zero_ne_zero {A : Type u_1} {B : Type u_2} [] [Ring B] [] [Algebra A B] {x : B} (hx : ) (h : x 0) :
(minpoly A x).coeff 0 0

The minimal polynomial of a nonzero element has nonzero constant coefficient.

theorem minpoly_algEquiv_toLinearMap {K : Type u_1} {L : Type u_2} [] [] [] [Algebra K L] (σ : L ≃ₐ[K] L) (hσ : ) :
minpoly K σ.toLinearMap = Polynomial.X ^ - Polynomial.C 1

The minimal polynomial (over K) of σ : Gal(L/K) is X ^ (orderOf σ) - 1.

theorem minpoly_algHom_toLinearMap {K : Type u_1} {L : Type u_2} [] [] [] [Algebra K L] (σ : L →ₐ[K] L) (hσ : ) :
minpoly K σ.toLinearMap = Polynomial.X ^ - Polynomial.C 1

The minimal polynomial (over K) of σ : Gal(L/K) is X ^ (orderOf σ) - 1.