mem_intermediateField_of_minpoly_splits

English

Let x ∈ L be integral over K. If the minimal polynomial of x over K splits over the intermediate field F, then x ∈ F.

Русский

Пусть x ∈ L интегрирован над K. Если минполином x над K распадается над промежуточным полем F, то x ∈ F.

LaTeX

$$$\\text{IsIntegral}_K(x) \\land \\text{Splits}(\\text{algebraMap } K F, \\minpoly_K(x)) \\Rightarrow x \\in F$$$

Lean4

theorem mem_intermediateField_of_minpoly_splits {x : L} (int : IsIntegral K x) {F : IntermediateField K L}
    (h : Splits (algebraMap K F) (minpoly K x)) : x ∈ F := by rw [← F.fieldRange_val];
  exact int.mem_range_algebraMap_of_minpoly_splits h

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