Theorems · Theorem · group theory

Equiv.Perm.isThreeCycle_sq_of_three_mem_cycleType_five

∀ {g : Equiv.Perm (Fin 5)}, 3 ∈ g.cycleType → (g * g).IsThreeCycle

Part of proving $A_5$ is simple. Shows that the square of any element of $A_5$ with a 3-cycle in its cycle decomposition is a 3-cycle, so the normal closure of the original element must be $A_5$.

Defined in

Mathlib.GroupTheory.SpecificGroups.Alternating

Cited by

0 results in Mathlib

Foundations

Depth 104 from the axioms · uses propext, Classical.choice, Quot.sound