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.
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 (is_integral 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
- minpoly A x = dite (is_integral A x) (Ξ» (hx : is_integral A x), _.min (Ξ» (p : polynomial A), p.monic β§ polynomial.evalβ (algebra_map A B) x p = 0) hx) (Ξ» (hx : Β¬is_integral A x), 0)
A minimal polynomial is monic.
A minimal polynomial is nonzero.
An element is a root of its minimal polynomial.
A minimal polynomial is not 1
.
A minimal polynomial is not a unit.
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.
The degree of a minimal polynomial, as a natural number, is positive.
The degree of a minimal polynomial is positive.
If B/A
is an injective ring extension, and a
is an element of A
,
then the minimal polynomial of algebra_map A B a
is X - C a
.
If a
strictly divides the minimal polynomial of x
, then x
cannot be a root for a
.
A minimal polynomial is irreducible.
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 gcd_domain_degree_le_of_ne_zero
which relaxes
the assumptions on A
in exchange for stronger assumptions on B
.
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.gcd_unique
which relaxes the
assumptions on A
in exchange for stronger assumptions on B
.
If an element x
is a root of a polynomial p
, then the minimal polynomial of x
divides p
.
See also minpoly.gcd_domain_dvd
which relaxes the assumptions on A
in exchange for stronger
assumptions on B
.
If y
is a conjugate of x
over a field K
, then it is a conjugate over a subring R
.
If y
is the image of x
in an extension, their minimal polynomials coincide.
We take h : y = algebra_map L T x
as an argument because rw h
typically fails
since is_integral R y
depends on y.
A technical finiteness result.
Equations
- minpoly.fintype.subtype_prod hX F = let hX : fintype β₯X := hX.fintype in pi.fintype
Function from Hom_K(E,L) to pi type Ξ (x : basis), roots of min poly of x
Equations
- minpoly.roots_of_min_poly_pi_type F E K Ο x = β¨βΟ βx, _β©
Given field extensions E/F
and K/F
, with E/F
finite, there are finitely many F
-algebra
homomorphisms E ββ[K] K
.
Equations
For GCD domains, the minimal polynomial over the ring is the same as the minimal polynomial
over the fraction field. See minpoly.gcd_domain_eq_field_fractions'
if S
is already a
K
-algebra.
For GCD domains, the minimal polynomial over the ring is the same as the minimal polynomial
over the fraction field. Compared to minpoly.gcd_domain_eq_field_fractions
, this version is useful
if the element is in a ring that is already a K
-algebra.
For GCD domains, the minimal polynomial divides any primitive polynomial that has the integral
element as root. See also minpoly.dvd
which relaxes the assumptions on S
in exchange for
stronger assumptions on R
.
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.degree_le_of_ne_zero
which relaxes the
assumptions on S
in exchange for stronger assumptions on R
.
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.unique
which relaxes the
assumptions on S
in exchange for stronger assumptions on R
.
If B/K
is a nontrivial algebra over a field, and x
is an element of K
,
then the minimal polynomial of algebra_map K B x
is X - C x
.
The minimal polynomial of 0
is X
.
The minimal polynomial of 1
is X - 1
.
A minimal polynomial is prime.
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.