English
If g ∈ Perm(5) has a 3-cycle in its cycle decomposition, then g^2 is a 3-cycle.
Русский
Если g ∈ Perm(5) имеет в разложении по циклам трёхциклическую часть, то g^2 является трёхциклом.
LaTeX
$$$$\\text{If } g \\in \\operatorname{Perm}(5) \\text{ and } 3 \\in \\operatorname{cycleType}(g),\\quad \\operatorname{IsThreeCycle}(g^2).$$$$
Lean4
/-- 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$. -/
theorem isThreeCycle_sq_of_three_mem_cycleType_five {g : Perm (Fin 5)} (h : 3 ∈ cycleType g) : IsThreeCycle (g * g) :=
by
obtain ⟨c, g', rfl, hd, _, h3⟩ := mem_cycleType_iff.1 h
simp only [mul_assoc]
rw [hd.commute.eq, ← mul_assoc g']
suffices hg' : orderOf g' ∣ 2 by
rw [← pow_two, orderOf_dvd_iff_pow_eq_one.1 hg', one_mul]
exact (card_support_eq_three_iff.1 h3).isThreeCycle_sq
rw [← lcm_cycleType, Multiset.lcm_dvd]
intro n hn
rw [le_antisymm (two_le_of_mem_cycleType hn) (le_trans (le_card_support_of_mem_cycleType hn) _)]
apply le_of_add_le_add_left
rw [← hd.card_support_mul, h3]
exact (c * g').support.card_le_univ
