Theorems · Theorem · field theory

minpoly.eq_of_linearIndependent

∀ (A : Type u_1) {B : Type u_2} [inst : CommRing A] [inst_1 : Ring B] [inst_2 : Algebra A B] (x : B) {p : Polynomial A},
  p.Monic →
    (Polynomial.aeval x) p = 0 → ∀ (n : ℕ), p.degree = ↑n → (LinearIndependent A fun i => x ^ ↑i) → minpoly A x = p

If a monic polynomial p : A[X] of degree n annihilates an element x in an A-algebra B, such that {xⁱ | 0 ≤ i < n} is linearly independent over A, then p is the minimal polynomial of x over A.

Defined in

Mathlib.FieldTheory.Minpoly.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingRingAlgebra