English
One can realize any group G as a subgroup of the symmetric group acting on G via a faithful action; Cayley’s theorem extends to any faithful action.
Русский
Любую группу G можно вложить в симметрическую группу, действующую на G, через верное действие; теорема Кэйли обобщена на случай верного действия.
LaTeX
$$$G\\simeq \\mathrm{MulAction}.\\mathrm{toPermHom}(G)\\,\\mathrm{range}$$$
Lean4
/-- **Cayley's theorem**: Every group G is isomorphic to a subgroup of the symmetric group acting on
`G`. Note that we generalize this to an arbitrary "faithful" group action by `G`. Setting `H = G`
recovers the usual statement of Cayley's theorem via `RightCancelMonoid.faithfulSMul` -/
noncomputable def subgroupOfMulAction (G H : Type*) [Group G] [MulAction G H] [FaithfulSMul G H] :
G ≃* (MulAction.toPermHom G H).range :=
MulEquiv.ofLeftInverse' _ (Classical.choose_spec MulAction.toPerm_injective.hasLeftInverse)
