exists_algHom_of_splits — Mathlib

English

Under the splitting conditions for all s ∈ E, there exists an algebra homomorphism φ: E →_F K extending f on L.

Русский

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

LaTeX

$$$\exists φ : E \to_F K, φ \circ (L \to E) = f$$$

Lean4

theorem exists_algHom_of_splits : ∃ φ : E →ₐ[F] K, φ.comp L.val = f :=
  exists_algHom_of_adjoin_splits (fun x _ ↦ hK' x) f (adjoin_univ F E)

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