doc(GroupTheory): mention Cayley's theorem by name (#32056)

Author: grunweg

Mathlib/GroupTheory/Perm/Subgroup.lean

@@ -20,6 +20,9 @@ It also provides decidable instances on membership in these subgroups, since
 `MonoidHom.decidableMemRange` cannot be inferred without the help of a lambda.
 The presence of these instances induces a `Fintype` instance on the `QuotientGroup.Quotient` of
 these subgroups.
+
+In particular, we prove **Cayley's theorem** in `Equiv.Perm.subgroupOfMulAction`:
+every group `G` is isomorphic to a subgroup of the symmetric group acting on `G`.
 -/
 
 @[expose] public section

docs/overview.yaml

@@ -49,6 +49,7 @@ General algebra:
     cyclic group: 'IsCyclic'
     nilpotent group: 'Group.IsNilpotent'
     permutation group of a type: 'Equiv.Perm'
+    Cayley's theorem: 'Equiv.Perm.subgroupOfMulAction'
     alternating group: 'alternatingGroup'
     A5 is simple: 'alternatingGroup.isSimpleGroup_five'
     classification of abelian simple groups: CommGroup.is_simple_iff_prime_card