ker_aeval_ring_hom'_unit_polynomial

English

For any endomorphism f and a unit polynomial c, the kernel of the polynomial evaluation aeval_f at c is {0}.

Русский

Для любого эндоморфизма f и единичного многочлена c ядро аппроксимации aeval_f(c) тривиально (содержит только нуль).

LaTeX

$$$$ \ker(\mathrm{aeval}_f(c)) = \{0\}. $$$$

Lean4

theorem ker_aeval_ring_hom'_unit_polynomial (f : End R M) (c : R[X]ˣ) : LinearMap.ker (aeval f (c : R[X])) = ⊥ :=
  LinearMap.ker_eq_bot'.mpr fun m hm ↦ by simpa [← mul_apply, ← aeval_mul] using congr(c⁻¹.1.aeval f $hm)

Похожие утверждения