Regular_Representations_in_Group_are_Permutations
Provedgroup-theoryproofwikiregular-representations
In a group, the left and right regular representations by any element are permutations (bijections).
Preamble
import Mathlib.Algebra.Group.Defs import Mathlib.Logic.Function.Basic
Formal statement
theorem Regular_Representations_in_Group_are_Permutations {G : Type _} [Group G] (a : G) : Function.Bijective (fun x => a * x) ∧ Function.Bijective (fun x => x * a) := by sorrySource