instIsScalarTower

Mathlib.NumberTheory.NumberField.Basic

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

English

There is a scalar tower IsScalarTower (𝓞_K) K L for any L that is a ring with a K-algebra structure.

Русский

Существует тензорная башня скаляров IsScalarTower (𝓞_K) K L для любого кольца L с K-алгеброй.

LaTeX

$$$\text{IsScalarTower } (\mathcal{O}_K) K L.$$$

Lean4

instance {L : Type*} [Ring L] [Algebra K L] : IsScalarTower (𝓞 K) K L :=
  inferInstanceAs (IsScalarTower (integralClosure _ _) K L)

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

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

Разделы

Аффилиация

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