English
The average element is invariant under right multiplication by group elements; equivalently, multiplying the averaging operator by any group element on the right fixes the average.
Русский
Среднее элемент инвариант относительно правого умножения на элементы группы; иначе говоря, произведение среднего оператора на правый элемент группы не изменяет среднее.
LaTeX
$$$$ average\;kG \cdot (Finsupp.single\;g\;1) = average\;kG. $$$$
Lean4
/-- `average k G` is invariant under right multiplication by elements of `G`.
-/
@[simp]
theorem mul_average_right (g : G) : average k G * ↑(Finsupp.single g 1) = average k G :=
by
simp only [mul_one, Finset.sum_mul, Algebra.smul_mul_assoc, average, MonoidAlgebra.of_apply,
MonoidAlgebra.single_mul_single]
set f : G → MonoidAlgebra k G := fun x => Finsupp.single x 1
change ⅟(Fintype.card G : k) • ∑ x : G, f (x * g) = ⅟(Fintype.card G : k) • ∑ x : G, f x
rw [Function.Bijective.sum_comp (Group.mulRight_bijective g) _]
