Theorems · Theorem · commutative algebra

Polynomial.monic_generator_eq_minpoly

∀ (𝕜 : Type u_1) {A : Type u_2} [inst : Field 𝕜] [inst_1 : Ring A] [inst_2 : Algebra 𝕜 A] (a : A) (p : Polynomial 𝕜),
  p.Monic → Ideal.span {p} = Polynomial.annIdeal 𝕜 a → Polynomial.annIdealGenerator 𝕜 a = p

If a monic generates the annihilating ideal, it must match our choice of the annihilating ideal generator.

Defined in

Mathlib.LinearAlgebra.AnnihilatingPolynomial

Cited by

0 results in Mathlib

Foundations

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

Assumes

FieldRingAlgebra