Cayley's theorem for monoids

• monoid_faithful_self — every monoid acts faithfully on itself: the left-regular representation MulAction.toEndHom : N →* Function.End N is injective.

theorem LeanPool.KrohnRhodes.monoid_faithful_self (N : Type u) [Monoid N] : Function.Injective ⇑MulAction.toEndHom

Every monoid acts faithfully on itself. The left-regular representation MulAction.toEndHom : N →* Function.End N (sending n to left-multiplication by n) is injective: n is recovered as the image of 1 under left-multiplication by n.