English
The normal closure of the 5-cycle finRotate 5 inside A_5 is the whole group.
Русский
Нормальное замыкание 5-цикла finRotate 5 внутри A_5 есть вся группа.
LaTeX
$$$$\\operatorname{normalClosure}\\{\\langle \\operatorname{finRotate}(5), \\operatorname{finRotate\_bit1\_mem\_alternatingGroup}(n := 2)\\rangle\\} = \\operatorname{top}.$$$
Lean4
/-- The normal closure of the 5-cycle `finRotate 5` within $A_5$ is the whole group. This will be
used to show that the normal closure of any 5-cycle within $A_5$ is the whole group. -/
theorem normalClosure_finRotate_five :
normalClosure ({⟨finRotate 5, finRotate_bit1_mem_alternatingGroup (n := 2)⟩} : Set (alternatingGroup (Fin 5))) =
⊤ :=
eq_top_iff.2
(by
have h3 : IsThreeCycle (Fin.cycleRange 2 * finRotate 5 * (Fin.cycleRange 2)⁻¹ * (finRotate 5)⁻¹) :=
card_support_eq_three_iff.1 (by decide)
rw [← h3.alternating_normalClosure (by rw [card_fin])]
refine normalClosure_le_normal ?_
rw [Set.singleton_subset_iff, SetLike.mem_coe]
have h :
(⟨finRotate 5, finRotate_bit1_mem_alternatingGroup (n := 2)⟩ : alternatingGroup (Fin 5)) ∈ normalClosure _ :=
SetLike.mem_coe.1
(subset_normalClosure (Set.mem_singleton _))
-- Porting note: added `:` to help the elaborator (otherwise we get a timeout)
exact
(mul_mem
(Subgroup.normalClosure_normal.conj_mem _ h
⟨Fin.cycleRange 2, Fin.isThreeCycle_cycleRange_two.mem_alternatingGroup⟩)
(inv_mem h) :))
