lcm_orderOf_eq_exponent — Mathlib

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))

Похожие утверждения