English
A finite group of prime order is cyclic.
Русский
Конечная группа простого порядка циклична.
LaTeX
$$IsCyclic(α) при Nat.card α = p и pPrime$$
Lean4
@[to_additive]
instance isCyclic [IsCyclic α] (H : Subgroup α) : IsCyclic H :=
haveI := Classical.propDecidable
let ⟨g, hg⟩ := IsCyclic.exists_generator (α := α)
if hx : ∃ x : α, x ∈ H ∧ x ≠ (1 : α) then
let ⟨x, hx₁, hx₂⟩ := hx
let ⟨k, hk⟩ := hg x
have hk : g ^ k = x := hk
have hex : ∃ n : ℕ, 0 < n ∧ g ^ n ∈ H :=
⟨k.natAbs, Nat.pos_of_ne_zero fun h => hx₂ <| by rw [← hk, Int.natAbs_eq_zero.mp h, zpow_zero],
by
rcases k with k | k
· rw [Int.ofNat_eq_coe, Int.natAbs_cast k, ← zpow_natCast, ← Int.ofNat_eq_coe, hk]
exact hx₁
· rw [Int.natAbs_negSucc, ← Subgroup.inv_mem_iff H]; simp_all⟩
⟨⟨⟨g ^ Nat.find hex, (Nat.find_spec hex).2⟩, fun ⟨x, hx⟩ =>
let ⟨k, hk⟩ := hg x
have hk : g ^ k = x := hk
have hk₂ : g ^ ((Nat.find hex : ℤ) * (k / Nat.find hex : ℤ)) ∈ H :=
by
rw [zpow_mul]
apply H.zpow_mem
exact mod_cast (Nat.find_spec hex).2
have hk₃ : g ^ (k % Nat.find hex : ℤ) ∈ H :=
(Subgroup.mul_mem_cancel_right H hk₂).1 <| by rw [← zpow_add, Int.emod_add_mul_ediv, hk]; exact hx
have hk₄ : k % Nat.find hex = (k % Nat.find hex).natAbs := by
rw [Int.natAbs_of_nonneg (Int.emod_nonneg _ (Int.natCast_ne_zero_iff_pos.2 (Nat.find_spec hex).1))]
have hk₅ : g ^ (k % Nat.find hex).natAbs ∈ H := by rwa [← zpow_natCast, ← hk₄]
have hk₆ : (k % (Nat.find hex : ℤ)).natAbs = 0 :=
by_contradiction fun h =>
Nat.find_min hex
(Int.ofNat_lt.1 <| by rw [← hk₄]; exact Int.emod_lt_of_pos _ (Int.natCast_pos.2 (Nat.find_spec hex).1))
⟨Nat.pos_of_ne_zero h, hk₅⟩
⟨k / (Nat.find hex : ℤ),
Subtype.ext_iff.2
(by
suffices g ^ ((Nat.find hex : ℤ) * (k / Nat.find hex : ℤ)) = x by simpa [zpow_mul]
rw [Int.mul_ediv_cancel' (Int.dvd_of_emod_eq_zero (Int.natAbs_eq_zero.mp hk₆)), hk])⟩⟩⟩
else
by
have : H = (⊥ : Subgroup α) :=
Subgroup.ext fun x => ⟨fun h => by simp at *; tauto, fun h => by rw [Subgroup.mem_bot.1 h]; exact H.one_mem⟩
subst this; infer_instance
