Theorems · Definition · field theory

minpoly

(A : Type u_1) → {B : Type u_2} → [inst : CommRing A] → [inst_1 : Ring B] → [Algebra A B] → 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 (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.

Defined in

Mathlib.FieldTheory.Minpoly.Basic

Cited by

439 results in Mathlib

Foundations

Depth 83 from the axioms, rests on 1,769 definitions · uses propext, Classical.choice, Quot.sound

Assumes

CommRingRingAlgebra