isScalarTower_self

Mathlib.Algebra.MonoidAlgebra.Module

URI: https://scilib.ai/kg/mathlib#AddMonoidAlgebra.isScalarTower_self

English

There is an IsScalarTower instance for AddMonoidAlgebra k G over R, inherited from MonoidAlgebra via Multiplicative G.

Русский

Для AddMonoidAlgebra k G существует IsScalarTower, наследуемый от MonoidAlgebra через Multiplicative G.

LaTeX

$$$$IsScalarTower\ R\ k[G]\ k[G].$$$$

Lean4

instance isScalarTower_self [IsScalarTower R k k] : IsScalarTower R k[G] k[G] :=
  @MonoidAlgebra.isScalarTower_self k (Multiplicative G) R _ _ _ _

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

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

Разделы

Аффилиация

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