Set_Equivalence_of_Regular_Representations
Provedgroup-theoryproofwikiregular-representations
If S is a finite subset of a group G, then |a*S| = |S| for any element a.
Preamble
import Mathlib.Data.Finset.Card import Mathlib.Algebra.Group.Defs
Formal statement
theorem Set_Equivalence_of_Regular_Representations {G : Type _} [Group G] [DecidableEq G] (a : G) (S : Finset G) : (S.image (fun x => a * x)).card = S.card := by sorrySource