instModuleSubtypeMem_1

Mathlib.FieldTheory.IntermediateField.Basic

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

English

There is an IsScalarTower on the subtype corresponding to S and T, i.e., the tower passes through the subtypes.

Русский

Существует IsScalarTower на подтипы, соответствующие S и T, то есть башня сохраняется при переходе через подтипы.

LaTeX

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

Lean4

instance : Module S T :=
  Algebra.toModule

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

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

Разделы

Аффилиация

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