exists_algHom_of_splits_of_aeval — Mathlib

English

If S generates an adjoin and all minimal polynomials split, there exists φ: adjoin_F S →_F K extending f and compatible with AEVAL conditions.

Русский

Если S генерирует адъюнкцию и все минимальные полиномы распадаются, существует φ: adjoin_F S →_F K, который расширяет f и удовлетворяет AEVAL-условиям.

LaTeX

$$$\exists φ : adjoin F S \to_F K, φ \circ inclusion(hL) = f$$$

Lean4

theorem exists_algHom_of_splits_of_aeval (hy : aeval y (minpoly F x) = 0) : ∃ φ : E →ₐ[F] K, φ x = y :=
  exists_algHom_of_adjoin_splits_of_aeval (fun x _ ↦ hK' x) (adjoin_univ F E) hy

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