nonempty_algHom_of_minpoly_eq — Mathlib

English

If for every x in E there exists y in K with minpoly F x = minpoly F y, then there exists a K-algebra homomorphism from E to K.

Русский

Если для каждого x ∈ E существует y ∈ K с равным minpoly(F, x) и minpoly(F, y), то существует K-алгебраический гомоморф из E в K.

LaTeX

$$$\\Bigl(\\forall x\\in E,\\; \\exists y\\in K,\\; minpoly\\ F\\ x = minpoly\\ F\\ y\\Bigr) \\Rightarrow \\exists \\varphi: E \\to_F K$$$

Lean4

theorem nonempty_algHom_of_minpoly_eq (h : ∀ x : E, ∃ y : K, minpoly F x = minpoly F y) : Nonempty (E →ₐ[F] K) :=
  nonempty_algHom_of_exist_roots fun x ↦
    have ⟨y, hy⟩ := h x;
    ⟨y, by rw [hy, minpoly.aeval]⟩

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