mem_range_algHom_of_minpoly_splits

English

If the minimal polynomial of x over K splits in L, then the minimal polynomial of −x also splits in L.

Русский

Если минимальный полином x над K распадается в L, то минимальный полином −x также распадается в L.

LaTeX

$$$\\text{Splits}(\\operatorname{algebraMap}_K^L, \\minpoly K x) \\Rightarrow \\text{Splits}(\\operatorname{algebraMap}_K^L, \\minpoly K (-x))$$$

Lean4

theorem mem_range_algHom_of_minpoly_splits (int : IsIntegral R x) (h : Splits (algebraMap R K) (minpoly R x))
    (f : K →ₐ[R] L) : x ∈ f.range :=
  show x ∈ Set.range f from
    Set.image_subset_range _ ((minpoly R x).rootSet K) <|
      by
      rw [image_rootSet h f, mem_rootSet']
      exact ⟨((minpoly.monic int).map _).ne_zero, minpoly.aeval R x⟩

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