English
Let G be a group of order p^2 where p is prime. Then G is not cyclic if and only if the exponent of G equals p.
Русский
Пусть G — группа порядка p^2, где p простое. Тогда G не циклична тогда и только тогда, когда экспонента G равна p.
LaTeX
$$$|G|=p^2\ \land\ p\ \text{prime} \Rightarrow \neg \operatorname{IsCyclic}(G) \iff \operatorname{exponent}(G)=p$$$
Lean4
/-- A group of order `p ^ 2` is not cyclic if and only if its exponent is `p`. -/
@[to_additive]
theorem not_isCyclic_iff_exponent_eq_prime [Group α] {p : ℕ} (hp : p.Prime) (hα : Nat.card α = p ^ 2) :
¬IsCyclic α ↔ Monoid.exponent α = p := by
-- G is a nontrivial fintype of cardinality `p ^ 2`
have : Finite α := Nat.finite_of_card_ne_zero (hα ▸ pow_ne_zero 2 hp.ne_zero)
have : Nontrivial α :=
Finite.one_lt_card_iff_nontrivial.mp
(hα ▸ one_lt_pow₀ hp.one_lt two_ne_zero)
/- in the forward direction, we apply `exponent_eq_prime_iff`, and the reverse direction follows
immediately because if `α` has exponent `p`, it has no element of order `p ^ 2`. -/
refine
⟨fun h_cyc ↦ (Monoid.exponent_eq_prime_iff hp).mpr fun g hg ↦ ?_, fun h_exp h_cyc ↦
by
obtain (rfl | rfl) := eq_zero_or_one_of_sq_eq_self <| hα ▸ h_exp ▸ (h_cyc.exponent_eq_card).symm
· exact Nat.not_prime_zero hp
· exact Nat.not_prime_one hp⟩
/- we must show every non-identity element has order `p`. By Lagrange's theorem, the only possible
orders of `g` are `1`, `p`, or `p ^ 2`. It can't be the former because `g ≠ 1`, and it can't
the latter because the group isn't cyclic. -/
have := (Nat.mem_divisors (m := p ^ 2)).mpr ⟨hα ▸ orderOf_dvd_natCard (x := g), by aesop⟩
have : ∃ a < 3, p ^ a = orderOf g := by simpa [Nat.divisors_prime_pow hp 2] using this
obtain ⟨a, ha, ha'⟩ := by simpa using this
interval_cases a
· exact False.elim <| hg <| orderOf_eq_one_iff.mp <| by simp_all
· simp_all
· exact False.elim <| h_cyc <| isCyclic_of_orderOf_eq_card g <| by cutsat
