ofMulDistribMulAction — Mathlib

English

The distributive action on Additive G yields the same formula for Additive elements as above: g acts by multiplication in Additive.

Русский

Распространённое действие на Additive G даёт аналогичную формулу: g действует умножением в Additive.

LaTeX

$$$\\text{ofMulDistribMulAction\\_apply\\_apply}(g,a) = a' \\text{ with } a' = g • a$$$

Lean4

/-- Turns a `CommGroup` `G` with a `MulDistribMulAction` of a monoid `M` into a
`ℤ`-linear `M`-representation on `Additive G`. -/
def ofMulDistribMulAction : Representation ℤ M (Additive G) :=
  (addMonoidEndRingEquivInt (Additive G) : AddMonoid.End (Additive G) →* _).comp
    ((monoidEndToAdditive G : _ →* _).comp (MulDistribMulAction.toMonoidEnd M G))

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