mathlib3 documentation

field_theory.minpoly.basic

Minimal polynomials #

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

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 ireducibility under the assumption B is a domain.

source
noncomputable def minpoly (A : Type u_1) {B : Type u_2} [comm_ring A] [ring B] [algebra A B] (x : B) :
polynomial A

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
source
theorem minpoly.monic {A : Type u_1} {B : Type u_2} [comm_ring A] [ring B] [algebra A B] {x : B} (hx : is_integral A x) :
(minpoly A x).monic

A minimal polynomial is monic.

source
theorem minpoly.ne_zero {A : Type u_1} {B : Type u_2} [comm_ring A] [ring B] [algebra A B] {x : B} [nontrivial A] (hx : is_integral A x) :
minpoly A x ≠ 0

A minimal polynomial is nonzero.

source
theorem minpoly.eq_zero {A : Type u_1} {B : Type u_2} [comm_ring A] [ring B] [algebra A B] {x : B} (hx : ¬is_integral A x) :
minpoly A x = 0
source
theorem minpoly.minpoly_alg_hom {A : Type u_1} {B : Type u_2} {B' : Type u_3} [comm_ring A] [ring B] [ring B'] [algebra A B] [algebra A B'] (f : B →ₐ[A] B') (hf : function.injective ⇑f) (x : B) :
minpoly A (⇑f x) = minpoly A x
source
@[simp]
theorem minpoly.minpoly_alg_equiv {A : Type u_1} {B : Type u_2} {B' : Type u_3} [comm_ring A] [ring B] [ring B'] [algebra A B] [algebra A B'] (f : B ≃ₐ[A] B') (x : B) :
minpoly A (⇑f x) = minpoly A x
source
@[simp]
theorem minpoly.aeval (A : Type u_1) {B : Type u_2} [comm_ring A] [ring B] [algebra A B] (x : B) :
⇑(polynomial.aeval x) (minpoly A x) = 0

An element is a root of its minimal polynomial.

source
theorem minpoly.ne_one (A : Type u_1) {B : Type u_2} [comm_ring A] [ring B] [algebra A B] (x : B) [nontrivial B] :
minpoly A x ≠ 1

A minimal polynomial is not 1.

source
theorem minpoly.map_ne_one (A : Type u_1) {B : Type u_2} [comm_ring A] [ring B] [algebra A B] (x : B) [nontrivial B] {R : Type u_3} [semiring R] [nontrivial R] (f : A →+* R) :
polynomial.map f (minpoly A x) ≠ 1
source
theorem minpoly.not_is_unit (A : Type u_1) {B : Type u_2} [comm_ring A] [ring B] [algebra A B] (x : B) [nontrivial B] :
¬is_unit (minpoly A x)

A minimal polynomial is not a unit.

source
theorem minpoly.mem_range_of_degree_eq_one (A : Type u_1) {B : Type u_2} [comm_ring A] [ring B] [algebra A B] (x : B) (hx : (minpoly A x).degree = 1) :
x ∈ (algebra_map A B).range
source
theorem minpoly.min (A : Type u_1) {B : Type u_2} [comm_ring A] [ring B] [algebra A B] (x : B) {p : polynomial A} (pmonic : p.monic) (hp : ⇑(polynomial.aeval x) p = 0) :
(minpoly A x).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.

source
theorem minpoly.unique' (A : Type u_1) {B : Type u_2} [comm_ring A] [ring B] [algebra A B] (x : B) {p : polynomial A} (hm : p.monic) (hp : ⇑(polynomial.aeval x) p = 0) (hl : ∀ (q : polynomial A), q.degree < p.degree → q = 0 ∨ ⇑(polynomial.aeval x) q ≠ 0) :
p = minpoly A x
source
theorem minpoly.subsingleton (A : Type u_1) {B : Type u_2} [comm_ring A] [ring B] [algebra A B] (x : B) [subsingleton B] :
minpoly A x = 1
source
theorem minpoly.nat_degree_pos {A : Type u_1} {B : Type u_2} [comm_ring A] [ring B] [algebra A B] {x : B} [nontrivial B] (hx : is_integral A x) :
0 < (minpoly A x).nat_degree

The degree of a minimal polynomial, as a natural number, is positive.

source
theorem minpoly.degree_pos {A : Type u_1} {B : Type u_2} [comm_ring A] [ring B] [algebra A B] {x : B} [nontrivial B] (hx : is_integral A x) :
0 < (minpoly A x).degree

The degree of a minimal polynomial is positive.

source
theorem minpoly.eq_X_sub_C_of_algebra_map_inj {A : Type u_1} {B : Type u_2} [comm_ring A] [ring B] [algebra A B] (a : A) (hf : function.injective ⇑(algebra_map A B)) :
minpoly A (⇑(algebra_map A B) a) = polynomial.X - ⇑polynomial.C a

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.

source
theorem minpoly.aeval_ne_zero_of_dvd_not_unit_minpoly {A : Type u_1} {B : Type u_2} [comm_ring A] [ring B] [algebra A B] {x : B} {a : polynomial A} (hx : is_integral A x) (hamonic : a.monic) (hdvd : dvd_not_unit a (minpoly A x)) :
⇑(polynomial.aeval x) a ≠ 0

If a strictly divides the minimal polynomial of x, then x cannot be a root for a.

source
theorem minpoly.irreducible {A : Type u_1} {B : Type u_2} [comm_ring A] [ring B] [algebra A B] {x : B} [is_domain A] [is_domain B] (hx : is_integral A x) :
irreducible (minpoly A x)

A minimal polynomial is irreducible.