instIsScalarTowerSubtypeMemIntermediateFieldNormalClosure_1

Mathlib.FieldTheory.Normal.Closure

URI: https://scilib.ai/kg/mathlib#normalClosure.instIsScalarTowerSubtypeMemIntermediateFieldNormalClosure_1

English

There is an IsScalarTower structure giving K acting on the normalClosure and L with the scalar actions compatible.

Русский

Существует структура IsScalarTower, обеспечивающая совместимость действия K на нормальном замыкании и на L.

LaTeX

$$$IsScalarTower\ K\ (\operatorname{normalClosure}(F,K,L))\ L$$$

Lean4

instance : IsScalarTower K (normalClosure F K L) L :=
  of_algebraMap_eq' rfl

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

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

Разделы

Аффилиация

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