nonempty_algHom_of_splits — Mathlib

English

There exists an F-algebra homomorphism from E to K extending a given L→K homomorphism under splitting hypotheses.

Русский

Существует F-алгебр-гомоморфизм из E в K, расширяющий заданный L→K гомоморфизм при условиях разложения.

LaTeX

$$$\exists φ : E \to_F K, φ \text{ extends } f$$$

Lean4

theorem nonempty_algHom_of_splits : Nonempty (E →ₐ[F] K) :=
  nonempty_algHom_of_adjoin_splits (fun x _ ↦ hK' x) (adjoin_univ F E)

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