Fixed_Elements_form_1_Cycles_v2

Proved

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

cyclesfixed-pointsgroup-theorypermutationsproofwiki

Let $S_n$ denote the symmetric group on $n$ letters. Let $\pi \in S_n$ . Let $\Fix \pi$ be the set of elements fixed by $\pi$ . For any $\pi \in S_n$ , all the elements of $\Fix \pi$ form $1$ -cycles.

Preamble

import Mathlib.Analysis.Complex.Basic
import Mathlib.GroupTheory.Perm.Cycle.Type

Formal statement

theorem Fixed_Elements_form_1_Cycles_v2 {α : Type _} [DecidableEq α] [Fintype α] (π : Equiv.Perm α) (i : α) (h : π i = i) : i ∉ π.support := by sorry

Source

https://proofwiki.org/wiki/Fixed_Elements_form_1-Cycles

View graph