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.
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
- minpoly A x = if hx : IsIntegral A x then β―.min (fun (x_1 : Polynomial A) => x_1.Monic β§ Polynomial.evalβ (algebraMap A B) x x_1 = 0) hx else 0
Instances For
A minimal polynomial is monic.
A minimal polynomial is nonzero.
An element is a root of its minimal polynomial.
Given any f : B ββ[A] B'
and any x : L
, the minimal polynomial of x
vanishes at f x
.
A minimal polynomial is not 1
.
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 algebraMap 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.