Composition_of_Regular_Representations
Provedproofwikiregular-representationssemigroups
In a semigroup, the composition of left regular representations satisfies λ_x ∘ λ_y = λ_{x*y}.
Preamble
import Mathlib.Algebra.Group.Defs
Formal statement
theorem Composition_of_Regular_Representations {S : Type _} [Semigroup S] (x y : S) : (fun z => x * (y * z)) = (fun z => (x * y) * z) := by sorrySource