English
Let α be a finite set with a decidable equality and cardinality a prime. If σ is a cycle with full support and τ is a transposition, then the closure of {σ, τ} in the permutation group on α is the whole group.
Русский
Пусть α – конечное множество с разрешённым равенством и простым кардиналом. Пусть σ – цикл с полной опорой, а τ — транспозиция; тогда замыкание {σ, τ} в группе перестановок на α есть вся группа.
LaTeX
$$$\\text{Nat.Prime}(|\\alpha|) ⟹ (IsCycle(σ) ∧ σ.support = univ ∧ IsSwap(τ)) ⟹ closure({σ, τ}) = top$$$
Lean4
theorem closure_prime_cycle_swap {σ τ : Perm α} (h0 : (Fintype.card α).Prime) (h1 : IsCycle σ)
(h2 : σ.support = Finset.univ) (h3 : IsSwap τ) : closure ({ σ, τ } : Set (Perm α)) = ⊤ :=
by
obtain ⟨x, y, h4, h5⟩ := h3
obtain ⟨i, hi⟩ :=
h1.exists_pow_eq (mem_support.mp ((Finset.ext_iff.mp h2 x).mpr (Finset.mem_univ x)))
(mem_support.mp ((Finset.ext_iff.mp h2 y).mpr (Finset.mem_univ y)))
rw [h5, ← hi]
refine closure_cycle_coprime_swap (Nat.Coprime.symm (h0.coprime_iff_not_dvd.mpr fun h => h4 ?_)) h1 h2 x
obtain ⟨m, hm⟩ := h
rwa [hm, pow_mul, ← Finset.card_univ, ← h2, ← h1.orderOf, pow_orderOf_eq_one, one_pow, one_apply] at hi
