Theorems · Definition · group theory

Representation.ofMulActionSelfAsModuleEquiv

{k : Type u_1} →
  {G : Type u_2} →
    [inst : CommSemiring k] →
      [inst_1 : Group G] → (Representation.ofMulAction k G G).asModule ≃ₗ[MonoidAlgebra k G] MonoidAlgebra k G

If we equip k[G] with the k-linear G-representation induced by the left regular action of G on itself, the resulting object is isomorphic as a k[G]-module to k[G] with its natural k[G]-module structure.

Defined in

Mathlib.RepresentationTheory.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommSemiringGroup