Endomorphism polynomials

DefinitionAnnihilating polynomials#

annIdeal R a is the annihilating ideal of all p : R[X] such that p(a) = 0.

The informal notation p(a) stands for Polynomial.aeval a p. Again informally, the annihilating ideal of a is { p ∈ R[X] | p(a) = 0 }. This is an ideal in R[X]. The formal definition uses the kernel of the aeval map.

Polynomial.annIdeal.{u_1, u_2} (R : Type u_1) {A : Type u_2} [CommSemiring R] [Semiring A]
  [Algebra R A] (a : A) : Ideal (Polynomial R)

Sources

• Mathlib documentation: Polynomial.annIdeal
• Source of Polynomial.annIdeal in Mathlib/LinearAlgebra/AnnihilatingPolynomial.lean
• Mathlib undergraduate list: Linear algebra › Endomorphism polynomials

MathlibPolynomial.annIdeal

Uses 4

Statement usesAssociative algebra over a commutative ring · Ideal of a commutative ring · Linear map · Polynomial in one indeterminate

• Minimal polynomial
• Characteristic polynomial
• Cayley-Hamilton theorem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.