feat: primality criteria for Monoid.exponent (#8723)

This PR shows a few facts related to `Monoid.exponent`, especially when it is prime:

1. A nontrivial finite cancellative monoid has exponent greater than 1.
2. A nontrivial monoid has prime exponent `p` if and only if every non-identity element has order `p`.
3. A group of order `p ^ 2` with `p` prime is not cyclic if and only if it has exponent `p`.

Mathlib/Algebra/GroupPower/Basic.lean

@@ -245,6 +245,10 @@ theorem dvd_pow_self (a : M) {n : ℕ} (hn : n ≠ 0) : a ∣ a ^ n :=
 
 end Monoid
 
+lemma eq_zero_or_one_of_sq_eq_self [CancelMonoidWithZero M] {x : M} (hx : x ^ 2 = x) :
+    x = 0 ∨ x = 1 :=
+  or_iff_not_imp_left.mpr (mul_left_injective₀ · <| by simpa [sq] using hx)
+
 /-!
 ### Commutative (additive) monoid
 -/

Mathlib/GroupTheory/Exponent.lean

@@ -236,6 +236,21 @@ theorem _root_.Nat.Prime.exists_orderOf_eq_pow_factorization_exponent {p : ℕ}
 #align nat.prime.exists_order_of_eq_pow_factorization_exponent Nat.Prime.exists_orderOf_eq_pow_factorization_exponent
 #align nat.prime.exists_order_of_eq_pow_padic_val_nat_add_exponent Nat.Prime.exists_addOrderOf_eq_pow_padic_val_nat_add_exponent
 
+/-- A nontrivial monoid has prime exponent `p` if and only if every non-identity element has
+order `p`. -/
+@[to_additive]
+lemma exponent_eq_prime_iff {G : Type*} [Monoid G] [Nontrivial G] {p : ℕ} (hp : p.Prime) :
+    Monoid.exponent G = p ↔ ∀ g : G, g ≠ 1 → orderOf g = p := by
+  refine ⟨fun hG g hg ↦ ?_, fun h ↦ dvd_antisymm ?_ ?_⟩
+  · rw [Ne.def, ← orderOf_eq_one_iff] at hg
+    exact Eq.symm <| (hp.dvd_iff_eq hg).mp <| hG ▸ Monoid.order_dvd_exponent g
+  · apply Monoid.exponent_dvd_of_forall_pow_eq_one G p fun g ↦ ?_
+    by_cases hg : g = 1
+    · simp [hg]
+    · simpa [h g hg] using pow_orderOf_eq_one g
+  · obtain ⟨g, hg⟩ := exists_ne (1 : G)
+    simpa [h g hg] using Monoid.order_dvd_exponent g
+
 variable {G}
 
 @[to_additive]
@@ -374,6 +389,23 @@ end CancelCommMonoid
 
 end Monoid
 
+section Group
+
+@[to_additive AddGroup.one_lt_exponent]
+lemma Group.one_lt_exponent [Group G] [Finite G] [Nontrivial G] :
+    1 < Monoid.exponent G := by
+  let _inst := Fintype.ofFinite G
+  obtain ⟨g, hg⟩ := exists_ne (1 : G)
+  rw [← Monoid.lcm_order_eq_exponent]
+  have hg' : 2 ≤ orderOf g := Nat.lt_of_le_of_ne (orderOf_pos g) <| by
+    simpa [eq_comm, orderOf_eq_one_iff] using hg
+  refine hg'.trans <| Nat.le_of_dvd ?_ <| Finset.dvd_lcm (by simp)
+  rw [Nat.pos_iff_ne_zero, Ne.def, Finset.lcm_eq_zero_iff]
+  rintro ⟨x, -, hx⟩
+  exact (orderOf_pos x).ne' hx
+
+end Group
+
 section CommGroup
 
 open Subgroup

Mathlib/GroupTheory/SpecificGroups/Cyclic.lean

@@ -651,4 +651,32 @@ protected theorem ZMod.exponent (n : ℕ) : AddMonoid.exponent (ZMod n) = n := b
   · rw [IsAddCyclic.exponent_eq_zero_of_infinite]
   · rw [IsAddCyclic.exponent_eq_card, card]
 
+/-- A group of order `p ^ 2` is not cyclic if and only if its exponent is `p`. -/
+@[to_additive]
+lemma 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`
+  let _inst : Fintype α := @Fintype.ofFinite α <| Nat.finite_of_card_ne_zero <| by aesop
+  have hα' : Fintype.card α = p ^ 2 := by simpa using hα
+  have := (Fintype.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_card (x := g), by aesop⟩
+  simp? [Nat.divisors_prime_pow hp 2] at this says
+    simp only [Nat.divisors_prime_pow hp 2, Finset.mem_map, Finset.mem_range,
+      Function.Embedding.coeFn_mk] at this
+  obtain ⟨a, ha, ha'⟩ := this
+  interval_cases a
+  · exact False.elim <| hg <| orderOf_eq_one_iff.mp <| by aesop
+  · aesop
+  · exact False.elim <| h_cyc <| isCyclic_of_orderOf_eq_card g <| by aesop
+
 end Exponent