splits_of_isScalarTower — Mathlib

English

If f splits over algebraMap R K and R, K, L form a scalar tower, then f splits over algebraMap R L.

Русский

Если f распадается над algebraMap R K и образующая башня скаляров выполняется, то f распадается над algebraMap R L.

LaTeX

$$$\forall f:Polynomial\ R[X],\ (Algebra\ K\ L) \land (IsScalarTower R K L) \Rightarrow (Splits (algebraMap R K) f) \Rightarrow Splits (algebraMap R L) f$$$

Lean4

theorem splits_of_isScalarTower {f : R[X]} [Algebra K L] [IsScalarTower R K L] (h : Splits (algebraMap R K) f) :
    Splits (algebraMap R L) f :=
  splits_of_algHom h (IsScalarTower.toAlgHom R K L)

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