Regular_Representation_of_Invertible_Element_is_Permutation
Provedmonoidsproofwikiregular-representations
In a monoid, if a is invertible, then the left and right regular representations by a are permutations (bijections).
Preamble
import Mathlib.Algebra.Group.Units.Basic import Mathlib.Logic.Function.Basic
Formal statement
theorem Regular_Representation_of_Invertible_Element_is_Permutation {M : Type _} [Monoid M] (a : M) (ha : IsUnit a) : Function.Bijective (fun x => a * x) ∧ Function.Bijective (fun x => x * a) := by sorrySource