Theorems · Theorem · group theory

GroupAlgebra.mul_average_left

∀ (k : Type u_1) (G : Type u_2) [inst : CommSemiring k] [inst_1 : Group G] [inst_2 : Fintype G]
  [inst_3 : Invertible ↑(Fintype.card G)] (g : G),
  MonoidAlgebra.single g 1 * GroupAlgebra.average k G = GroupAlgebra.average k G

average k G is invariant under left multiplication by elements of G.

Defined in

Mathlib.RepresentationTheory.Invariants

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringGroupFintypeInvertible