ofMulAction_single — Mathlib

English

Under the distribution action, applying g to a acts by g•a on Additive G in the additive endomorphism sense.

Русский

При распределённом действии действие g на a даёт результат g•a в добавочно-модульном смысле.

LaTeX

$$$\\text{ofMulDistribMulAction}(k,G,A)\\ g\\ a = g \\cdot a$$$

Lean4

@[simp]
theorem ofMulAction_single (g : G) (x : H) (r : k) :
    ofMulAction k G H g (Finsupp.single x r) = Finsupp.single (g • x) r :=
  Finsupp.mapDomain_single

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