English
In a nontrivial ring, the polynomial X − C r is not a unit.
Русский
В не тривиальном кольце многочлен X − C r не является единицей.
LaTeX
$$¬IsUnit (X - C r)$$
Lean4
/-- The evaluation map is not generally multiplicative when the coefficient ring is noncommutative,
but nevertheless any polynomial of the form `p * (X - monomial 0 r)` is sent to zero
when evaluated at `r`.
This is the key step in our proof of the Cayley-Hamilton theorem.
-/
theorem eval_mul_X_sub_C {p : R[X]} (r : R) : (p * (X - C r)).eval r = 0 :=
by
simp only [eval, eval₂_eq_sum, RingHom.id_apply]
have bound :=
calc
(p * (X - C r)).natDegree ≤ p.natDegree + (X - C r).natDegree := natDegree_mul_le
_ ≤ p.natDegree + 1 := (add_le_add_left (natDegree_X_sub_C_le _) _)
_ < p.natDegree + 2 := lt_add_one _
rw [sum_over_range' _ _ (p.natDegree + 2) bound]
swap
· simp
rw [sum_range_succ']
conv_lhs =>
congr
arg 2
simp [coeff_mul_X_sub_C, sub_mul, mul_assoc, ← pow_succ']
rw [sum_range_sub']
simp
