smulCommClass'

Mathlib.GroupTheory.GroupAction.ConjAct

URI: https://scilib.ai/kg/mathlib#ConjAct.smulCommClass'

← MathLib Explorer

English

There is an instance giving ConjAct G a MulDistribMulAction structure on G.

Русский

Существует инстанс, задающий ConjAct G структуру MulDistribMulAction над G.

LaTeX

$$$\text{instance }\text{ MulDistribMulAction } (ConjAct G) G$$$

Lean4

instance smulCommClass' [SMul α G] [SMulCommClass G α G] [IsScalarTower α G G] : SMulCommClass (ConjAct G) α G :=
  haveI := SMulCommClass.symm G α G
  SMulCommClass.symm _ _ _

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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