Prove2Me

Set_of_Permutations_is_Largest_Effective_Transformation_Group

Proved

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

group-theorypermutationsproofwikitransformation-groups

The set of permutations of a set XX forms the largest effective transformation group of XX.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Set_of_Permutations_is_Largest_Effective_Transformation_Group {X : Type _} [DecidableEq X] [Fintype X] : Function.Injective (MulAction.toPermHom (Equiv.Perm X) X) := by sorry
Source
https://proofwiki.org/wiki/Set_of_Permutations_is_Largest_Effective_Transformation_Group

View graph