# Minimal polynomials #

This file defines the minimal polynomial of an element x of an A-algebra B, under the assumption that x is integral over A, and derives some basic properties such as irreducibility under the assumption B is a domain.

noncomputable def minpoly (A : Type u_1) {B : Type u_2} [] [Ring B] [Algebra A B] (x : B) :

Suppose x : B, where B is an A-algebra.

The minimal polynomial minpoly A x of x is a monic polynomial with coefficients in A of smallest degree that has x as its root, if such exists (IsIntegral A x) or zero otherwise.

For example, if V is a π-vector space for some field π and f : V ββ[π] V then the minimal polynomial of f is minpoly π f.

Equations
Instances For
theorem minpoly.monic {A : Type u_1} {B : Type u_2} [] [Ring B] [Algebra A B] {x : B} (hx : ) :
(minpoly A x).Monic

A minimal polynomial is monic.

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

A minimal polynomial is nonzero.

theorem minpoly.eq_zero {A : Type u_1} {B : Type u_2} [] [Ring B] [Algebra A B] {x : B} (hx : Β¬) :
minpoly A x = 0
theorem minpoly.algHom_eq {A : Type u_1} {B : Type u_2} {B' : Type u_3} [] [Ring B] [Ring B'] [Algebra A B] [Algebra A B'] (f : B ββ[A] B') (hf : ) (x : B) :
minpoly A (f x) = minpoly A x
theorem minpoly.algebraMap_eq {A : Type u_1} {B' : Type u_3} [] [Ring B'] [Algebra A B'] {B : Type u_4} [] [Algebra A B] [Algebra B B'] [IsScalarTower A B B'] (h : Function.Injective β(algebraMap B B')) (x : B) :
minpoly A ((algebraMap B B') x) = minpoly A x
@[simp]
theorem minpoly.algEquiv_eq {A : Type u_1} {B : Type u_2} {B' : Type u_3} [] [Ring B] [Ring B'] [Algebra A B] [Algebra A B'] (f : B ββ[A] B') (x : B) :
minpoly A (f x) = minpoly A x
@[simp]
theorem minpoly.aeval (A : Type u_1) {B : Type u_2} [] [Ring B] [Algebra A B] (x : B) :
() (minpoly A x) = 0

An element is a root of its minimal polynomial.

@[simp]
theorem minpoly.aeval_algHom (A : Type u_1) {B : Type u_2} {B' : Type u_3} [] [Ring B] [Ring B'] [Algebra A B] [Algebra A B'] (f : B ββ[A] B') (x : B) :
(Polynomial.aeval (f x)) (minpoly A x) = 0

Given any f : B ββ[A] B' and any x : L, the minimal polynomial of x vanishes at f x.

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

A minimal polynomial is not 1.

theorem minpoly.map_ne_one (A : Type u_1) {B : Type u_2} [] [Ring B] [Algebra A B] (x : B) [] {R : Type u_4} [] [] (f : A β+* R) :
theorem minpoly.not_isUnit (A : Type u_1) {B : Type u_2} [] [Ring B] [Algebra A B] (x : B) [] :

A minimal polynomial is not a unit.

theorem minpoly.mem_range_of_degree_eq_one (A : Type u_1) {B : Type u_2} [] [Ring B] [Algebra A B] (x : B) (hx : (minpoly A x).degree = 1) :
x β ().range
theorem minpoly.min (A : Type u_1) {B : Type u_2} [] [Ring B] [Algebra A B] (x : B) {p : } (pmonic : p.Monic) (hp : () p = 0) :
(minpoly A x).degree β€ p.degree

The defining property of the minimal polynomial of an element x: it is the monic polynomial with smallest degree that has x as its root.

theorem minpoly.unique' (A : Type u_1) {B : Type u_2} [] [Ring B] [Algebra A B] (x : B) {p : } (hm : p.Monic) (hp : () p = 0) (hl : β (q : ), q.degree < p.degree β q = 0 β¨ () q β  0) :
p = minpoly A x
theorem minpoly.subsingleton (A : Type u_1) {B : Type u_2} [] [Ring B] [Algebra A B] (x : B) [] :
minpoly A x = 1
theorem minpoly.natDegree_pos {A : Type u_1} {B : Type u_2} [] [Ring B] [Algebra A B] {x : B} [] (hx : ) :
0 < (minpoly A x).natDegree

The degree of a minimal polynomial, as a natural number, is positive.

theorem minpoly.degree_pos {A : Type u_1} {B : Type u_2} [] [Ring B] [Algebra A B] {x : B} [] (hx : ) :
0 < (minpoly A x).degree

The degree of a minimal polynomial is positive.

theorem minpoly.degree_eq_one_iff {A : Type u_1} {B : Type u_2} [] [Ring B] [Algebra A B] {x : B} [] :
(minpoly A x).degree = 1 β x β ().range
theorem minpoly.natDegree_eq_one_iff {A : Type u_1} {B : Type u_2} [] [Ring B] [Algebra A B] {x : B} [] :
(minpoly A x).natDegree = 1 β x β ().range
theorem minpoly.two_le_natDegree_iff {A : Type u_1} {B : Type u_2} [] [Ring B] [Algebra A B] {x : B} [] (int : ) :
2 β€ (minpoly A x).natDegree β x β ().range
theorem minpoly.two_le_natDegree_subalgebra {A : Type u_1} [] {B : Type u_4} [] [Algebra A B] [] {S : } {x : B} (int : IsIntegral (β₯S) x) :
2 β€ (minpoly (β₯S) x).natDegree β x β S
theorem minpoly.eq_X_sub_C_of_algebraMap_inj {A : Type u_1} {B : Type u_2} [] [Ring B] [Algebra A B] (a : A) (hf : Function.Injective β()) :
minpoly A (() a) = Polynomial.X - Polynomial.C a

If B/A is an injective ring extension, and a is an element of A, then the minimal polynomial of algebraMap A B a is X - C a.

theorem minpoly.aeval_ne_zero_of_dvdNotUnit_minpoly {A : Type u_1} {B : Type u_2} [] [Ring B] [Algebra A B] {x : B} {a : } (hx : ) (hamonic : a.Monic) (hdvd : DvdNotUnit a (minpoly A x)) :
() a β  0

If a strictly divides the minimal polynomial of x, then x cannot be a root for a.

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

A minimal polynomial is irreducible.