∀ (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), (GroupAlgebra.average k G * fun₀ | g => 1) = GroupAlgebra.average k G