English
If α is a finite commutative group and exponent α = card α, then α is cyclic.
Русский
Если коммутативная группа конечна и показатель степени равен кардиналу, то группа циклична.
LaTeX
$$exponent α = Nat.card α → IsCyclic α$$
Lean4
@[to_additive]
theorem prime_card [Finite α] : (Nat.card α).Prime :=
by
have h0 : 0 < Nat.card α := Nat.card_pos
obtain ⟨g, hg⟩ := IsCyclic.exists_generator (α := α)
rw [Nat.prime_def]
refine ⟨Finite.one_lt_card_iff_nontrivial.2 inferInstance, fun n hn => ?_⟩
refine (IsSimpleOrder.eq_bot_or_eq_top (Subgroup.zpowers (g ^ n))).symm.imp ?_ ?_
· intro h
have hgo := orderOf_pow (n := n) g
rw [orderOf_eq_card_of_forall_mem_zpowers hg, Nat.gcd_eq_right_iff_dvd.2 hn, orderOf_eq_card_of_forall_mem_zpowers,
eq_comm, Nat.div_eq_iff_eq_mul_left (Nat.pos_of_dvd_of_pos hn h0) hn] at hgo
· exact (mul_left_cancel₀ (ne_of_gt h0) ((mul_one (Nat.card α)).trans hgo)).symm
· intro x
rw [h]
exact Subgroup.mem_top _
· intro h
apply le_antisymm (Nat.le_of_dvd h0 hn)
rw [← orderOf_eq_card_of_forall_mem_zpowers hg]
apply orderOf_le_of_pow_eq_one (Nat.pos_of_dvd_of_pos hn h0)
rw [← Subgroup.mem_bot, ← h]
exact Subgroup.mem_zpowers _
