Identity_Permutation_is_Disjoint_from_All_v2

Proved

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

disjointgroup-theoryidentitypermutationsproofwiki

Let $S_n$ denote the symmetric group on $n$ letters. Let $e \in S_n$ be the identity permutation on $S_n$ . Then $e$ is disjoint from every permutation $\pi$ on $S_n$ (including itself).

Preamble

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

Formal statement

theorem Identity_Permutation_is_Disjoint_from_All_v2 {α : Type _} [DecidableEq α] [Fintype α] (σ : Equiv.Perm α) : Equiv.Perm.Disjoint 1 σ := by sorry

Source

https://proofwiki.org/wiki/Identity_Permutation_is_Disjoint_from_All

View graph