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.


minimal_polynomial

Let B be an A-algebra, and x an element of B that is integral over A. The minimal polynomial of x is a monic polynomial of smallest degree that has x as its root.

minimal_polynomial.monic

A minimal polynomial is monic.

minimal_polynomial.aeval

An element is a root of its minimal polynomial.

minimal_polynomial.min

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.

minimal_polynomial.ne_zero

A minimal polynomial is nonzero.

minimal_polynomial.degree_le_of_ne_zero

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.

minimal_polynomial.unique

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.

minimal_polynomial.dvd

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

minimal_polynomial.degree_ne_zero

The degree of a minimal polynomial is nonzero.

minimal_polynomial.not_is_unit

A minimal polynomial is not a unit.

minimal_polynomial.degree_pos

The degree of a minimal polynomial is positive.

minimal_polynomial.prime

A minimal polynomial is prime.

minimal_polynomial.irreducible

A minimal polynomial is irreducible.

minimal_polynomial.algebra_map

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.

minimal_polynomial.algebra_map'

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.

minimal_polynomial.zero

The minimal polynomial of 0 is X.

minimal_polynomial.one

The minimal polynomial of 1 is X - 1.

minimal_polynomial.root

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.

minimal_polynomial.coeff_zero_eq_zero

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

minimal_polynomial.coeff_zero_ne_zero

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