instIsScalarTower_1

Mathlib.NumberTheory.NumberField.Basic

URI: https://scilib.ai/kg/mathlib#NumberField.RingOfIntegers.instIsScalarTower_1

English

There is a natural IsScalarTower structure: 𝓞_K → 𝓞_L → L.

Русский

Существует естественная структура IsScalarTower: 𝓞_K → 𝓞_L → L.

LaTeX

$$$IsScalarTower(\\mathcal{O}_K)(\\mathcal{O}_L)L$$$

Lean4

instance : IsScalarTower (𝓞 K) (𝓞 L) L :=
  IsScalarTower.of_algebraMap_eq' rfl

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

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

Разделы

Аффилиация

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