# mathlibdocumentation

field_theory.minimal_polynomial

# 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.

After stating the defining property we specialize to the setting of field extensions and derive some well-known properties, amongst which the fact that minimal polynomials are irreducible, and uniquely determined by their defining property.

def minimal_polynomial {α : Type u} {β : Type v} [comm_ring α] [ring β] [ β] {x : β} :
x

Let B be an A-algebra, and x an element of B that is integral over A so we have some term hx : is_integral A x. The minimal polynomial minimal_polynomial hx of x is a monic polynomial of smallest degree that has x as its root. For instance, if V is a K-vector space for some field K, and f : V →ₗ[K] V then the minimal polynomial of f is minimal_polynomial f.is_integral.

Equations
• = minimal_polynomial._proof_1.min (λ (p : , p.monic x p = 0) hx
theorem minimal_polynomial.monic {α : Type u} {β : Type v} [comm_ring α] [ring β] [ β] {x : β} (hx : x) :

A minimal polynomial is monic.

@[simp]
theorem minimal_polynomial.aeval {α : Type u} {β : Type v} [comm_ring α] [ring β] [ β] {x : β} (hx : x) :
= 0

An element is a root of its minimal polynomial.

theorem minimal_polynomial.min {α : Type u} {β : Type v} [comm_ring α] [ring β] [ β] {x : β} (hx : x) {p : polynomial α} :
p.monic p = 0.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 minimal_polynomial.ne_zero {α : Type u} {β : Type v} [field α] [ring β] [ β] {x : β} (hx : x) :

A minimal polynomial is nonzero.

theorem minimal_polynomial.degree_le_of_ne_zero {α : Type u} {β : Type v} [field α] [ring β] [ β] {x : β} (hx : x) {p : polynomial α} :
p 0 p = 0.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.

theorem minimal_polynomial.unique {α : Type u} {β : Type v} [field α] [ring β] [ β] {x : β} (hx : x) {p : polynomial α} :
p.monic p = 0(∀ (q : , q.monic q = 0p.degree q.degree)

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.

theorem minimal_polynomial.dvd {α : Type u} {β : Type v} [field α] [ring β] [ β] {x : β} (hx : x) {p : polynomial α} :
p = 0

If an element x is a root of a polynomial p, then the minimal polynomial of x divides p.

theorem minimal_polynomial.dvd_map_of_is_scalar_tower {α : Type u_1} {γ : Type u_2} (β : Type u_3) [comm_ring α] [field β] [comm_ring γ] [ β] [ γ] [ γ] [ γ] {x : γ} (hx : x) :

theorem minimal_polynomial.degree_ne_zero {α : Type u} {β : Type v} [field α] [ring β] [ β] {x : β} (hx : x) [nontrivial β] :

The degree of a minimal polynomial is nonzero.

theorem minimal_polynomial.not_is_unit {α : Type u} {β : Type v} [field α] [ring β] [ β] {x : β} (hx : x) [nontrivial β] :

A minimal polynomial is not a unit.

theorem minimal_polynomial.degree_pos {α : Type u} {β : Type v} [field α] [ring β] [ β] {x : β} (hx : x) [nontrivial β] :

The degree of a minimal polynomial is positive.

theorem minimal_polynomial.unique' {α : Type u} {β : Type v} [field α] [ring β] [ β] {x : β} (hx : x) [nontrivial β] {p : polynomial α} :
p = 0p.monic

@[simp]
theorem minimal_polynomial.algebra_map {α : Type u} {β : Type v} [field α] [ring β] [ β] [nontrivial β] (a : α) (ha : ( β) a)) :

If L/K is a field extension, and x is an element of L in the image of K, then the minimal polynomial of x is X - C x.

theorem minimal_polynomial.algebra_map' {α : Type u} (β : Type v) [field α] [ring β] [ β] [nontrivial β] (a : α) :

If L/K is a field extension, and x is an element of L in the image of K, then the minimal polynomial of x is X - C x.

@[simp]
theorem minimal_polynomial.zero {α : Type u} {β : Type v} [field α] [ring β] [ β] [nontrivial β] {h₀ : 0} :

The minimal polynomial of 0 is X.

@[simp]
theorem minimal_polynomial.one {α : Type u} {β : Type v} [field α] [ring β] [ β] [nontrivial β] {h₁ : 1} :

The minimal polynomial of 1 is X - 1.

theorem minimal_polynomial.prime {α : Type u} {β : Type v} [field α] [domain β] [ β] {x : β} (hx : x) :

A minimal polynomial is prime.

theorem minimal_polynomial.irreducible {α : Type u} {β : Type v} [field α] [domain β] [ β] {x : β} (hx : x) :

A minimal polynomial is irreducible.

theorem minimal_polynomial.root {α : Type u} {β : Type v} [field α] [domain β] [ β] {x : β} (hx : x) {y : α} :
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 minimal_polynomial.coeff_zero_eq_zero {α : Type u} {β : Type v} [field α] [domain β] [ β] {x : β} (hx : x) :
.coeff 0 = 0 x = 0

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

theorem minimal_polynomial.coeff_zero_ne_zero {α : Type u} {β : Type v} [field α] [domain β] [ β] {x : β} (hx : x) :
x 0.coeff 0 0

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