Theorems · Definition · group theory

Rep.free

(k : Type u) → (G : Type v) → [inst : CommRing k] → [inst_1 : Monoid G] → Type u' → Rep.{max (max u u') v, u, v} k G

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

Defined in

Mathlib.RepresentationTheory.Rep.Basic

Cited by

9 results in Mathlib

Foundations

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

Assumes

CommRingMonoid