# mathlib3documentation

field_theory.minpoly.field

# Minimal polynomials on an algebra over a field #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file specializes the theory of minpoly to the setting of field extensions and derives some well-known properties, amongst which the fact that minimal polynomials are irreducible, and uniquely determined by their defining property.

theorem minpoly.degree_le_of_ne_zero (A : Type u_1) {B : Type u_2} [field A] [ring B] [ B] (x : B) {p : polynomial A} (pnz : p 0) (hp : p = 0) :

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.

theorem minpoly.ne_zero_of_finite_field_extension (A : Type u_1) {B : Type u_2} [field A] [ring B] [ B] (e : B) [ B] :
e 0
theorem minpoly.unique (A : Type u_1) {B : Type u_2} [field A] [ring B] [ B] (x : B) {p : polynomial A} (pmonic : p.monic) (hp : p = 0) (pmin : (q : , q.monic q = 0 p.degree q.degree) :
p = x

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.

theorem minpoly.dvd (A : Type u_1) {B : Type u_2} [field A] [ring B] [ B] (x : B) {p : polynomial A} (hp : p = 0) :
x p

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.

theorem minpoly.dvd_map_of_is_scalar_tower (A : Type u_1) (K : Type u_2) {R : Type u_3} [comm_ring A] [field K] [comm_ring R] [ K] [ R] [ R] [ R] (x : R) :
x (minpoly A x)
theorem minpoly.dvd_map_of_is_scalar_tower' (R : Type u_1) {S : Type u_2} (K : Type u_3) (L : Type u_4) [comm_ring R] [comm_ring S] [field K] [comm_ring L] [ S] [ K] [ L] [ L] [ L] [ L] [ L] (s : S) :
( L) s) (minpoly R s)
theorem minpoly.aeval_of_is_scalar_tower (R : Type u_1) {K : Type u_2} {T : Type u_3} {U : Type u_4} [comm_ring R] [field K] [comm_ring T] [ K] [ T] [ T] [ T] [ U] [ U] [ U] (x : T) (y : U) (hy : (minpoly K x) = 0) :
(minpoly R x) = 0

If y is a conjugate of x over a field K, then it is a conjugate over a subring R.

theorem minpoly.eq_of_irreducible_of_monic {A : Type u_1} {B : Type u_2} [field A] [ring B] [ B] {x : B} [nontrivial B] {p : polynomial A} (hp1 : irreducible p) (hp2 : p = 0) (hp3 : p.monic) :
p = x
theorem minpoly.eq_of_irreducible {A : Type u_1} {B : Type u_2} [field A] [ring B] [ B] {x : B} [nontrivial B] {p : polynomial A} (hp1 : irreducible p) (hp2 : p = 0) :
= x
theorem minpoly.eq_of_algebra_map_eq {K : Type u_1} {S : Type u_2} {T : Type u_3} [field K] [comm_ring S] [comm_ring T] [ S] [ T] [ T] [ T] (hST : function.injective T)) {x : S} {y : T} (hx : x) (h : y = T) x) :
x = y

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.

theorem minpoly.add_algebra_map {A : Type u_1} [field A] {B : Type u_2} [comm_ring B] [ B] {x : B} (hx : x) (a : A) :
(x + B) a) = (minpoly A x).comp
theorem minpoly.sub_algebra_map {A : Type u_1} [field A] {B : Type u_2} [comm_ring B] [ B] {x : B} (hx : x) (a : A) :
(x - B) a) = (minpoly A x).comp
noncomputable def minpoly.fintype.subtype_prod {E : Type u_1} {X : set E} (hX : X.finite) {L : Type u_2} (F : E ) :
fintype (Π (x : X), {l // l F x})

A technical finiteness result.

Equations
def minpoly.roots_of_min_poly_pi_type (F : Type u_3) (E : Type u_4) (K : Type u_5) [field F] [ring E] [comm_ring K] [is_domain K] [ E] [ K] [ E] (φ : E →ₐ[F] K) (x : ) :
{l // l (polynomial.map K) (minpoly F x.val)).roots}

Function from Hom_K(E,L) to pi type Π (x : basis), roots of min poly of x

Equations
theorem minpoly.aux_inj_roots_of_min_poly (F : Type u_3) (E : Type u_4) (K : Type u_5) [field F] [ring E] [comm_ring K] [is_domain K] [ E] [ K] [ E] :
@[protected, instance]
noncomputable def minpoly.alg_hom.fintype (F : Type u_3) (E : Type u_4) (K : Type u_5) [field F] [ring E] [comm_ring K] [is_domain K] [ E] [ K] [ E] :

Given field extensions E/F and K/F, with E/F finite, there are finitely many F-algebra homomorphisms E →ₐ[K] K.

Equations
theorem minpoly.eq_X_sub_C {A : Type u_1} (B : Type u_2) [field A] [ring B] [ B] [nontrivial B] (a : A) :
( B) a) =

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.

theorem minpoly.eq_X_sub_C' {A : Type u_1} [field A] (a : A) :
@[simp]
theorem minpoly.zero (A : Type u_1) (B : Type u_2) [field A] [ring B] [ B] [nontrivial B] :

The minimal polynomial of 0 is X.

@[simp]
theorem minpoly.one (A : Type u_1) (B : Type u_2) [field A] [ring B] [ B] [nontrivial B] :
1 =

The minimal polynomial of 1 is X - 1.

theorem minpoly.prime {A : Type u_1} {B : Type u_2} [field A] [ring B] [is_domain B] [ B] {x : B} (hx : x) :

A minimal polynomial is prime.

theorem minpoly.root {A : Type u_1} {B : Type u_2} [field A] [ring B] [is_domain B] [ B] {x : B} (hx : x) {y : A} (h : (minpoly A x).is_root y) :
B) 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 minpoly.coeff_zero_eq_zero {A : Type u_1} {B : Type u_2} [field A] [ring B] [is_domain B] [ B] {x : B} (hx : x) :
(minpoly A x).coeff 0 = 0 x = 0

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

theorem minpoly.coeff_zero_ne_zero {A : Type u_1} {B : Type u_2} [field A] [ring B] [is_domain B] [ B] {x : B} (hx : x) (h : x 0) :
(minpoly A x).coeff 0 0

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