Theorems · Definition · group theory

Representation.ofMulAction

(k : Type u_1) →
  [inst : Semiring k] →
    (G : Type u_2) → [inst_1 : Monoid G] → (H : Type u_3) → [MulAction G H] → Representation k G (MonoidAlgebra k H)

A G-action on H induces a representation G →* End(k[H]) in the natural way.

Defined in

Mathlib.RepresentationTheory.Basic

Cited by

15 results in Mathlib

Foundations

Depth 83 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemiringMonoidMulAction