ofMulDistribMulAction_apply_apply

English

In the action on Additive G, applying g to a corresponds to the additive action by g on a's underlying group.

Русский

В действии на Additive G применение g к a соотносится с добавочным действием g на группу, лежащую в основе a.

LaTeX

$$$(ofMulDistribMulAction\\; M\\ G\\ A)\\ g\\ a = g • a$$$

Lean4

@[simp]
theorem ofMulDistribMulAction_apply_apply (g : M) (a : Additive G) :
    ofMulDistribMulAction M G g a = Additive.ofMul (g • a.toMul) :=
  rfl

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