English
The exponent equals the Infimum of the set {d > 0 | ∀ x ∈ G, x^d = 1}. If no such d exists, exponent is 0.
Русский
Экспонента равна Infimum множества {d>0 | ∀ x ∈ G, x^d = 1}; если такого d нет, экспонента равна 0.
LaTeX
$$$\\operatorname{exponent}(G) = \\mathrm{Inf}\\{d\\in\\mathbb{N} \\mid d>0 \\wedge \\forall x\\in G, x^d=1\\}$$$
Lean4
@[to_additive]
theorem exponent_eq_sInf : Monoid.exponent G = sInf {d : ℕ | 0 < d ∧ ∀ x : G, x ^ d = 1} :=
by
by_cases h : Monoid.ExponentExists G
· have h' : {d : ℕ | 0 < d ∧ ∀ x : G, x ^ d = 1}.Nonempty := h
rw [Monoid.exponent, dif_pos h, Nat.sInf_def h']
congr
· have : {d | 0 < d ∧ ∀ (x : G), x ^ d = 1} = ∅ := Set.eq_empty_of_forall_notMem fun n hn ↦ h ⟨n, hn⟩
rw [Monoid.exponent_eq_zero_iff.mpr h, this, Nat.sInf_empty]
