English
For any endomorphism f and a unit polynomial c, the kernel of the AlgHom-coe of Polynomial.aeval f at c is zero.
Русский
Для любого эндоморфизма f и единичного многочлена c ядро соответствующего отображения через aeval равно нулю.
LaTeX
$$$$ \ker(\mathrm{AlgHom}.funLike.coe(\mathrm{Polynomial.aeval}\;f)\;c). = \{0\}. $$$$
Lean4
theorem aeval_apply_of_hasEigenvector {f : End R M} {p : R[X]} {μ : R} {x : M} (h : f.HasEigenvector μ x) :
aeval f p x = p.eval μ • x := by
refine p.induction_on ?_ ?_ ?_
· intro a; simp [Module.algebraMap_end_apply]
· intro p q hp hq; simp [hp, hq, add_smul]
· intro n a hna
rw [mul_comm, pow_succ', mul_assoc, map_mul, Module.End.mul_apply, mul_comm, hna]
simp only [mem_eigenspace_iff.1 h.1, smul_smul, aeval_X, eval_mul, eval_C, eval_pow, eval_X, LinearMap.map_smulₛₗ,
RingHom.id_apply, mul_comm]
