ofDistribMulAction_apply_apply

Mathlib.RepresentationTheory.Basic

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

English

The action of g on a in the distributive action case is given by the same left action as above on A.

Русский

Действие g на a в случае DistribMulAction задаётся тем же левым действием на A, как и выше.

LaTeX

$$$\\mathrm{ofDistribMulAction}(k,G,A)\\ g\\ a = g • a$$$

Lean4

@[simp]
theorem ofDistribMulAction_apply_apply (g : G) (a : A) : ofDistribMulAction k G A g a = g • a :=
  rfl

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

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

Разделы

Аффилиация

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