English
A nontrivial monoid has prime exponent p if and only if every non-identity element has order p.
Русский
Непустый моноид имеет простую экспоненту p тогда и только тогда каждый ненейтральный элемент имеет порядок p.
LaTeX
$$$\\\\operatorname{exponent} G = p \\\\iff \\\\forall g : G, g \\\\neq 1 \\\\Rightarrow \\\\operatorname{orderOf} g = p$$$
Lean4
/-- A nontrivial monoid has prime exponent `p` if and only if every non-identity element has
order `p`. -/
@[to_additive]
theorem 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, ← orderOf_eq_one_iff] at hg
exact Eq.symm <| (hp.dvd_iff_eq hg).mp <| hG ▸ Monoid.order_dvd_exponent g
· rw [exponent_dvd]
intro g
by_cases hg : g = 1
· simp [hg]
· rw [h g hg]
· obtain ⟨g, hg⟩ := exists_ne (1 : G)
simpa [h g hg] using Monoid.order_dvd_exponent g
