ofMulAction_def

Mathlib.RepresentationTheory.Basic

URI: https://scilib.ai/kg/mathlib#Representation.ofMulAction_def

English

The action of g on a basis element δ_x maps to δ_{g•x}; i.e., the image of the delta at x is the delta at g•x.

Русский

Действие g на базисный элемент δ_x переходит в δ_{g•x}.

LaTeX

$$$\\operatorname{ofMulAction}(k,G,H)\\ g\\ (\\mathsf{Finsupp.single\\;x\\;r}) = \\mathsf{Finsupp.single\\; (g·x)\\; r}$$$

Lean4

theorem ofMulAction_def (g : G) : ofMulAction k G H g = Finsupp.lmapDomain k k (g • ·) :=
  rfl

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

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

Разделы

Аффилиация

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