nonempty_algHom_of_adjoin_splits — Mathlib

English

There exists an F-algebra homomorphism from E to K, given the splitting conditions for S and adjoining settings.

Русский

Существование алгебр-гомоморфизма из E в K при заданных условиях разложения и адъюнкции.

LaTeX

$$$\exists φ : E \to_F K$$$

Lean4

theorem nonempty_algHom_of_adjoin_splits : Nonempty (E →ₐ[F] K) :=
  have ⟨φ, _⟩ := exists_algHom_of_adjoin_splits hK (⊥ : Lifts F E K).emb hS;
  ⟨φ⟩

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