lcm_orderOf_dvd_exponent — Mathlib

English

In a finite monoid G, the least common multiple of the orders of all elements divides the exponent of G.

Русский

В конечном моноиде G наименьшее общее кратное порядков всех элементов делит экспоненту G.

LaTeX

$$$\\operatorname{lcm}_{g \\in G} \\operatorname{orderOf} g \\\\mid \\operatorname{exponent} G$$$

Lean4

@[to_additive]
theorem lcm_orderOf_dvd_exponent [Fintype G] : (Finset.univ : Finset G).lcm orderOf ∣ exponent G :=
  by
  apply Finset.lcm_dvd
  intro g _
  exact order_dvd_exponent g

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