Theorems · Theorem · field theory

minpoly.unique

∀ (A : Type u_1) {B : Type u_2} [inst : Field A] [inst_1 : Ring B] [inst_2 : Algebra A B] (x : B) {p : Polynomial A},
  p.Monic →
    (Polynomial.aeval x) p = 0 →
      (∀ (q : Polynomial A), q.Monic → (Polynomial.aeval x) q = 0 → p.degree ≤ q.degree) → p = minpoly A 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.IsIntegrallyClosed.Minpoly.unique which relaxes the assumptions on A in exchange for stronger assumptions on B.

Defined in

Mathlib.FieldTheory.Minpoly.Field

Cited by

7 results in Mathlib

Foundations

Depth 112 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldRingAlgebra