Theorems · Theorem · field theory

Polynomial.eval_mul_X_sub_C

∀ {R : Type u} [inst : Ring R] {p : Polynomial R} (r : R), Polynomial.eval r (p * (Polynomial.X - Polynomial.C r)) = 0

The evaluation map is not generally multiplicative when the coefficient ring is noncommutative, but nevertheless any polynomial of the form p * (X - C r) is sent to zero when evaluated at r. This is the key step in our proof of the Cayley-Hamilton theorem.

Defined in

Mathlib.Algebra.Polynomial.AlgebraMap

Cited by

2 results in Mathlib

Foundations

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

Assumes

Ring