isScalarTower_mid — Mathlib

English

Let S be an intermediate field of L over K. Then there is an IsScalarTower K (Subtype {x ∈ S}) R.

Русский

Пусть S — промежуточное поле L над K. Тогда существует IsScalarTower K (пользуемся подтипом) R.

LaTeX

$$$\\text{IsScalarTower} K \\bigl(\\text{Subtype }\\{x : L \\mid x \\in S\\}\\bigr)\\; R$$$

Lean4

instance isScalarTower_mid {R : Type*} [Semiring R] [Algebra L R] [Algebra K R] [IsScalarTower K L R] :
    IsScalarTower K S R :=
  IsScalarTower.subalgebra' _ _ _ S.toSubalgebra

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