mathlib3

8e3deffc - feat(representation_theory/invariants): average_map is a projection onto the subspace of invariants (#14167)