English
For a commutative monoid G, exponent G equals the supremum of the orders of all elements, i.e., exponent G = sup_{g∈G} orderOf g.
Русский
В коммутативном моноиде экспонента равна верхней границе для порядков всех элементов: exponent G = sup_{g∈G} orderOf g.
LaTeX
$$$\\\\operatorname{exponent} G = \\\\sup_{g : G} \\\\operatorname{orderOf} g$$$
Lean4
@[to_additive]
theorem exponent_eq_iSup_orderOf (h : ∀ g : G, 0 < orderOf g) : exponent G = ⨆ g : G, orderOf g :=
by
rw [iSup]
by_cases ExponentExists G
case neg he =>
rw [← exponent_eq_zero_iff] at he
rw [he, Set.Infinite.Nat.sSup_eq_zero <| (exponent_eq_zero_iff_range_orderOf_infinite h).1 he]
case pos he =>
rw [csSup_eq_of_forall_le_of_forall_lt_exists_gt (Set.range_nonempty _)]
· simp_rw [Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff]
exact orderOf_le_exponent he
intro x hx
obtain ⟨g, hg⟩ := exists_orderOf_eq_exponent he
rw [← hg] at hx
simp_rw [Set.mem_range, exists_exists_eq_and]
exact ⟨g, hx⟩
