mathlib docs: field_theory.minimal

def minimal_polynomial {α : Type u} {β : Type v} [comm_ring α] [ring β] [algebra α β] {x : β} (hx : is_integral α x) :

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.

Equations

minimal_polynomial hx = minimal_polynomial._proof_1.min (λ (p : polynomial α), p.monic ∧ polynomial.eval₂ (algebra_map α β) x p = 0) hx

source

theorem minimal_polynomial.monic {α : Type u} {β : Type v} [comm_ring α] [ring β] [algebra α β] {x : β} (hx : is_integral α x) :

(minimal_polynomial hx).monic

A minimal polynomial is monic.

source

@[simp]

theorem minimal_polynomial.aeval {α : Type u} {β : Type v} [comm_ring α] [ring β] [algebra α β] {x : β} (hx : is_integral α x) :

⇑(polynomial.aeval x) (minimal_polynomial hx) = 0

An element is a root of its minimal polynomial.

source

theorem minimal_polynomial.min {α : Type u} {β : Type v} [comm_ring α] [ring β] [algebra α β] {x : β} (hx : is_integral α x) {p : polynomial α} (pmonic : p.monic) (hp : ⇑(polynomial.aeval x) p = 0) :

(minimal_polynomial hx).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 minimal_polynomial.ne_zero {α : Type u} {β : Type v} [field α] [ring β] [algebra α β] {x : β} (hx : is_integral α x) :

minimal_polynomial hx ≠ 0

A minimal polynomial is nonzero.

source

theorem minimal_polynomial.degree_le_of_ne_zero {α : Type u} {β : Type v} [field α] [ring β] [algebra α β] {x : β} (hx : is_integral α x) {p : polynomial α} (pnz : p ≠ 0) (hp : ⇑(polynomial.aeval x) p = 0) :

(minimal_polynomial hx).degree ≤ p.degree

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.

source

theorem minimal_polynomial.unique {α : Type u} {β : Type v} [field α] [ring β] [algebra α β] {x : β} (hx : is_integral α x) {p : polynomial α} (pmonic : p.monic) (hp : ⇑(polynomial.aeval x) p = 0) (pmin : ∀ (q : polynomial α), q.monic → ⇑(polynomial.aeval x) q = 0 → p.degree ≤ q.degree) :

p = minimal_polynomial hx

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.

source

theorem minimal_polynomial.dvd {α : Type u} {β : Type v} [field α] [ring β] [algebra α β] {x : β} (hx : is_integral α x) {p : polynomial α} (hp : ⇑(polynomial.aeval x) p = 0) :

minimal_polynomial hx ∣ p

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

source

theorem minimal_polynomial.dvd_map_of_is_scalar_tower {α : Type u_1} {γ : Type u_2} (β : Type u_3) [comm_ring α] [field β] [comm_ring γ] [algebra α β] [algebra α γ] [algebra β γ] [is_scalar_tower α β γ] {x : γ} (hx : is_integral α x) :

minimal_polynomial _ ∣ polynomial.map (algebra_map α β) (minimal_polynomial hx)

source

theorem minimal_polynomial.degree_ne_zero {α : Type u} {β : Type v} [field α] [ring β] [algebra α β] {x : β} (hx : is_integral α x) [nontrivial β] :

(minimal_polynomial hx).degree ≠ 0

The degree of a minimal polynomial is nonzero.

source

theorem minimal_polynomial.not_is_unit {α : Type u} {β : Type v} [field α] [ring β] [algebra α β] {x : β} (hx : is_integral α x) [nontrivial β] :

¬is_unit (minimal_polynomial hx)

A minimal polynomial is not a unit.

source

theorem minimal_polynomial.degree_pos {α : Type u} {β : Type v} [field α] [ring β] [algebra α β] {x : β} (hx : is_integral α x) [nontrivial β] :

0 < (minimal_polynomial hx).degree

The degree of a minimal polynomial is positive.

source

theorem minimal_polynomial.unique' {α : Type u} {β : Type v} [field α] [ring β] [algebra α β] {x : β} (hx : is_integral α x) [nontrivial β] {p : polynomial α} (hp1 : irreducible p) (hp2 : ⇑(polynomial.aeval x) p = 0) (hp3 : p.monic) :

p = minimal_polynomial hx

source

@[simp]

theorem minimal_polynomial.algebra_map {α : Type u} {β : Type v} [field α] [ring β] [algebra α β] [nontrivial β] (a : α) (ha : is_integral α (⇑(algebra_map α β) a)) :

minimal_polynomial ha = polynomial.X - ⇑polynomial.C a

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.

source

theorem minimal_polynomial.algebra_map' {α : Type u} (β : Type v) [field α] [ring β] [algebra α β] [nontrivial β] (a : α) :

minimal_polynomial is_integral_algebra_map = polynomial.X - ⇑polynomial.C a

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.

source

@[simp]

theorem minimal_polynomial.zero {α : Type u} {β : Type v} [field α] [ring β] [algebra α β] [nontrivial β] {h₀ : is_integral α 0} :

minimal_polynomial h₀ = polynomial.X

The minimal polynomial of 0 is X.

source

@[simp]

theorem minimal_polynomial.one {α : Type u} {β : Type v} [field α] [ring β] [algebra α β] [nontrivial β] {h₁ : is_integral α 1} :

minimal_polynomial h₁ = polynomial.X - 1

The minimal polynomial of 1 is X - 1.

source

theorem minimal_polynomial.prime {α : Type u} {β : Type v} [field α] [domain β] [algebra α β] {x : β} (hx : is_integral α x) :

prime (minimal_polynomial hx)

A minimal polynomial is prime.

source

theorem minimal_polynomial.irreducible {α : Type u} {β : Type v} [field α] [domain β] [algebra α β] {x : β} (hx : is_integral α x) :

irreducible (minimal_polynomial hx)

A minimal polynomial is irreducible.

source

theorem minimal_polynomial.root {α : Type u} {β : Type v} [field α] [domain β] [algebra α β] {x : β} (hx : is_integral α x) {y : α} (h : (minimal_polynomial hx).is_root y) :

⇑(algebra_map α β) 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.

source

@[simp]

theorem minimal_polynomial.coeff_zero_eq_zero {α : Type u} {β : Type v} [field α] [domain β] [algebra α β] {x : β} (hx : is_integral α x) :

(minimal_polynomial hx).coeff 0 = 0 ↔ x = 0

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

source

theorem minimal_polynomial.coeff_zero_ne_zero {α : Type u} {β : Type v} [field α] [domain β] [algebra α β] {x : β} (hx : is_integral α x) (h : x ≠ 0) :

(minimal_polynomial hx).coeff 0 ≠ 0

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

mathlib documentation

Minimal polynomials