mem_range_algebraMap_of_minpoly_splits

English

Let int be IsIntegral over R for x, and h: Splits (algebraMap R K) (minpoly R x). Then for any f: K →ₐ[R] L, x ∈ range f.

Русский

Пусть x интегрирован над R и minpoly R x распадается в K, тогда для любого гомоморфизма f: K →ₐ[R] L элемент x принадлежит образу f.

LaTeX

$$$\\forall f: K \\toₐ[R] L:\\ x \\in \\operatorname{range}(f)$$$

Lean4

theorem mem_range_algebraMap_of_minpoly_splits [Algebra K L] [IsScalarTower R K L] (int : IsIntegral R x)
    (h : Splits (algebraMap R K) (minpoly R x)) : x ∈ (algebraMap K L).range :=
  int.mem_range_algHom_of_minpoly_splits h (IsScalarTower.toAlgHom R K L)

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