aeval_algHom_eq_zero — Mathlib

English

If ϕ is an AdjoinRoot-algebra hom, then aeval (ϕ(root f)) f = 0; i.e., the image of root f under ϕ is a root of f in S.

Русский

Если ϕ — алгеброморф из AdjoinRoot f, то aeval (ϕ(root f)) f = 0; образ корня f под ϕ является корнем f в S.

LaTeX

$$$\\mathrm{aeval}(\\ϕ(\\mathrm{root} f))\\ f = 0$$$

Lean4

@[simp]
theorem aeval_algHom_eq_zero (ϕ : AdjoinRoot f →ₐ[R] S) : aeval (ϕ (root f)) f = 0 :=
  by
  have h : ϕ.toRingHom.comp (of f) = algebraMap R S := RingHom.ext_iff.mpr ϕ.commutes
  rw [aeval_def, ← h, ← RingHom.map_zero ϕ.toRingHom, ← eval₂_root f, hom_eval₂]
  rfl

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