instIsScalarTowerSubtypeMem_1

Mathlib.FieldTheory.IntermediateField.Basic

URI: https://scilib.ai/kg/mathlib#IntermediateField.instIsScalarTowerSubtypeMem_1

English

There is an IsScalarTower K (Subtype mem S) (Subtype mem T) given appropriate algebra structures.

Русский

Существует IsScalarTower K (Subtype mem S) (Subtype mem T) при надлежащих алгебраических структурах.

LaTeX

$$$\\text{IsScalarTower } K (\\text{Subtype mem } S) (\\text{Subtype mem } T)$$$

Lean4

instance [Algebra K E] [IsScalarTower K L E] : IsScalarTower K S T :=
  T.isScalarTower

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru