Theorems · Definition · group theory

GroupAlgebra.average

(k : Type u_1) →
  (G : Type u_2) →
    [inst : CommSemiring k] → [Group G] → [inst_2 : Fintype G] → [Invertible ↑(Fintype.card G)] → MonoidAlgebra k G

The average of all elements of the group G, considered as an element of k[G].

Defined in

Mathlib.RepresentationTheory.Invariants

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommSemiringGroupFintypeInvertible