Theorems · Definition · group theory

Representation.ofMulDistribMulAction

(M : Type u_1) →
  (G : Type u_2) →
    [inst : Monoid M] → [inst_1 : CommGroup G] → [MulDistribMulAction M G] → Representation ℤ M (Additive G)

Turns a CommGroup G with a MulDistribMulAction of a monoid M into a ℤ-linear M-representation on Additive G.

Defined in

Mathlib.RepresentationTheory.Basic

Cited by

2 results in Mathlib

Foundations

Depth 45 from the axioms · uses propext, Quot.sound

Assumes

MonoidCommGroupMulDistribMulAction