Theorems · Theorem · commutative algebra

Polynomial.annIdealGenerator_mem

∀ (𝕜 : Type u_1) {A : Type u_2} [inst : Field 𝕜] [inst_1 : Ring A] [inst_2 : Algebra 𝕜 A] (a : A),
  Polynomial.annIdealGenerator 𝕜 a ∈ Polynomial.annIdeal 𝕜 a

The annihilating ideal generator is a member of the annihilating ideal.

Defined in

Mathlib.LinearAlgebra.AnnihilatingPolynomial

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldRingAlgebra