English
In a finite monoid G, the least common multiple of the orders of all elements equals the exponent of G.
Русский
В конечном моноиде N НОК порядков всех элементов равен экспоненте G.
LaTeX
$$$\\operatorname{lcm}_{g \\in G} \\operatorname{orderOf} g = \\operatorname{exponent} G$$$
Lean4
@[to_additive]
theorem lcm_orderOf_eq_exponent [Fintype G] : (Finset.univ : Finset G).lcm orderOf = exponent G :=
Nat.dvd_antisymm (lcm_orderOf_dvd_exponent G) (exponent_dvd.mpr fun g => Finset.dvd_lcm (Finset.mem_univ g))