isScalarTower

Mathlib.FieldTheory.Galois.Basic

URI: https://scilib.ai/kg/mathlib#IntermediateField.fixedField.isScalarTower

English

There is a natural IsScalarTower structure linking K, fixedField(fixingSubgroup K), and E.

Русский

Существует естественная связка IsScalarTower между K, fixedField(fixingSubgroup K) и E.

LaTeX

$$$\text{IsScalarTower } K\, (\operatorname{fixedField}(\operatorname{fixingSubgroup}(K)))\, E$$$

Lean4

instance isScalarTower : IsScalarTower K (fixedField (fixingSubgroup K)) E :=
  ⟨fun _ _ _ => mul_assoc _ _ _⟩

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

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

Разделы

Аффилиация

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