Theorems · Definition · group theory

Representation.free

(k : Type u_6) →
  (G : Type u_7) →
    [inst : CommSemiring k] → [inst_1 : Monoid G] → (α : Type u_8) → Representation k G (α →₀ MonoidAlgebra k G)

The representation on α →₀ k[G] defined pointwise by the left regular representation.

Defined in

Mathlib.RepresentationTheory.Basic

Cited by

14 results in Mathlib

Foundations

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

Assumes

CommSemiringMonoid