Cayleys_Representation_Theorem

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

cayley-theoremgroup-theoryproofwikirepresentationsymmetric-groups

Let $S_n$ denote the symmetric group on $n$ letters. Every finite group is isomorphic to a subgroup of $S_n$ for some $n \in \Z$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Cayleys_Representation_Theorem {G : Type _} [Group G] [Fintype G] [DecidableEq G] : ∃ f : G →* Equiv.Perm G, Function.Injective f := by sorry

Source