Theorems · Definition · group theory

Rep.ofDistribMulAction

(k : Type u) →
  (G : Type v) →
    [inst : Ring k] →
      [inst_1 : Monoid G] →
        (A : Type w') →
          [inst_2 : AddCommGroup A] →
            [inst_3 : Module k A] → [inst_4 : DistribMulAction G A] → [SMulCommClass G k A] → Rep.{w', u, v} k G

Turns a k-module A with a compatible DistribMulAction of a monoid G into a k-linear G-representation on A.

Defined in

Mathlib.RepresentationTheory.Rep.Basic

Cited by

17 results in Mathlib

Foundations

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

Assumes

RingMonoidAddCommGroupModuleDistribMulActionSMulCommClass