Center_of_Symmetric_Group_is_Trivial_v2_retry
Provedproofwikiretry
The center of the symmetric group on n>=3 elements is trivial.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Center_of_Symmetric_Group_is_Trivial_v2_retry {α : Type _} [DecidableEq α] [Fintype α] (h : 3 ≤ Fintype.card α) : Subgroup.center (Equiv.Perm α) = ⊥ := by sorry