algHom_eq — Mathlib

English

For any A-algebra hom f: B → B', minpoly_A(f(x)) = minpoly_A(x).

Русский

Для любого A-алгебрового гомоморфа f: B → B' минимальный многочлен удовлетворяет minpoly_A(f(x)) = minpoly_A(x).

LaTeX

$$$\\minpoly_{A}(f(x)) = \\minpoly_{A}(x).$$$

Lean4

theorem algHom_eq (f : B →ₐ[A] B') (hf : Function.Injective f) (x : B) : minpoly A (f x) = minpoly A x := by
  classical
    simp_rw [minpoly, isIntegral_algHom_iff _ hf, ← Polynomial.aeval_def, aeval_algHom, AlgHom.comp_apply,
    _root_.map_eq_zero_iff f hf]

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