English
If a subgroup H of Perm α contains a swap and the size of α is prime and divides the size of H, then H is the whole group.
Русский
Если подгруппа H перестановок α содержит транспозицию и |α| — простое, а |α| делит |H|, тогда H = ⊤.
LaTeX
$$subgroup_eq_top_of_swap_mem h0 h1 h2 h3$$
Lean4
theorem subgroup_eq_top_of_swap_mem [DecidableEq α] {H : Subgroup (Perm α)} [d : DecidablePred (· ∈ H)] {τ : Perm α}
(h0 : (Fintype.card α).Prime) (h1 : Fintype.card α ∣ Fintype.card H) (h2 : τ ∈ H) (h3 : IsSwap τ) : H = ⊤ :=
by
haveI : Fact (Fintype.card α).Prime := ⟨h0⟩
obtain ⟨σ, hσ⟩ := exists_prime_orderOf_dvd_card (Fintype.card α) h1
have hσ1 : orderOf (σ : Perm α) = Fintype.card α := (Subgroup.orderOf_coe σ).trans hσ
have hσ2 : IsCycle ↑σ := isCycle_of_prime_order'' h0 hσ1
have hσ3 : (σ : Perm α).support = ⊤ := Finset.eq_univ_of_card (σ : Perm α).support (hσ2.orderOf.symm.trans hσ1)
have hσ4 : Subgroup.closure {↑σ, τ} = ⊤ := closure_prime_cycle_swap h0 hσ2 hσ3 h3
rw [eq_top_iff, ← hσ4, Subgroup.closure_le, Set.insert_subset_iff, Set.singleton_subset_iff]
exact ⟨Subtype.mem σ, h2⟩
