aeval_algHom — Mathlib

English

For any F-alg algebra hom f: B → B', the aeval of minpoly_A x by f(x) vanishes.

Русский

Для любого F-алгебрового гомоморфа f: B → B' значение aeval(f(x)) применительно к minpoly_A x равно 0.

LaTeX

$$$\\big(Polynomial.aeval (f(x))\\big)(\\minpoly_{A}(x)) = 0.$$$

Lean4

/-- Given any `f : B →ₐ[A] B'` and any `x : L`, the minimal polynomial of `x` vanishes at `f x`. -/
@[simp]
theorem aeval_algHom (f : B →ₐ[A] B') (x : B) : (Polynomial.aeval (f x)) (minpoly A x) = 0 := by
  rw [Polynomial.aeval_algHom, AlgHom.coe_comp, comp_apply, aeval, map_zero]

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