instIsScalarTowerCore

Mathlib.RingTheory.Extension.Presentation.Core

URI: https://scilib.ai/kg/mathlib#Algebra.Presentation.instIsScalarTowerCore

English

The core subalgebra P.Core sits inside a scalar tower with R and S, meaning the action of R on S factors through P.Core.

Русский

Ядро P образует скалярную башню с R и S, то есть действие R на S факторизуется через P.Core.

LaTeX

$$$\\mathrm{IsScalarTower}(P^{\\mathrm{Core}}, R, S)$$$

Lean4

instance : IsScalarTower P.Core R S :=
  inferInstanceAs <| IsScalarTower P.core R S

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

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

Разделы

Аффилиация

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