Prove2Me

Center_of_Symmetric_Group_is_Trivial

Proved

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

center-of-symmetric-group-is-trivialcenters-of-groupsproofwikisymmetric-groups

Let n be a natural number >= 3. Then the center of the symmetric group S_n is trivial.

Preamble
import Mathlib.GroupTheory.Perm.Basic
import Mathlib.GroupTheory.SpecificGroups.Cyclic
import Mathlib.GroupTheory.Subgroup.Center
Formal statement
theorem Center_of_Symmetric_Group_is_Trivial {α : Type*} [DecidableEq α] [Fintype α] (h : 3 ≤ Fintype.card α) : Subgroup.center (Equiv.Perm α) = ⊥ := by sorry
Source
https://proofwiki.org/wiki/Center_of_Symmetric_Group_is_Trivial

View graph