ofModuleMonoidAlgebra_obj_ρ

Mathlib.RepresentationTheory.Rep

URI: https://scilib.ai/kg/mathlib#Rep.ofModuleMonoidAlgebra_obj_ρ

← MathLib Explorer

English

The ρ-map on the object of ModuleMonoidAlgebra is the Representation.ofModule on M.

Русский

Отображение ρ на объекте ModuleMonoidAlgebra равно Representation.ofModule M.

LaTeX

$$$$ (ofModuleMonoidAlgebra.obj M).\\rho = Representation.ofModule M $$$$

Lean4

theorem ofModuleMonoidAlgebra_obj_ρ (M : ModuleCat.{u} (MonoidAlgebra k G)) :
    (ofModuleMonoidAlgebra.obj M).ρ = Representation.ofModule M :=
  rfl

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

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

Разделы

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

Аффилиация

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