minpoly_splits_tower_top — Mathlib

English

Let R ⊆ K ⊆ L with IsIntegral R x and tower relations; if Splits (algebraMap R L) (minpoly R x), then Splits (algebraMap K L) (minpoly K x).

Русский

Пусть R ⊆ K ⊆ L, x интегрирован над R и имеется тензорная башня; если minpoly R x распадается в L, тогда minpoly K x распадается в L.

LaTeX

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

Lean4

theorem minpoly_splits_tower_top [Algebra K L] [Algebra R L] [IsScalarTower R K L] (int : IsIntegral R x)
    (h : Splits (algebraMap R L) (minpoly R x)) : Splits (algebraMap K L) (minpoly K x) :=
  by
  rw [IsScalarTower.algebraMap_eq R K L] at h
  exact int.minpoly_splits_tower_top' h

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