English
For a finite monoid G, the exponent equals the maximum of the orders of its elements.
Русский
Для конечного моноида G экспонента равна максимальному порядку элемента в G.
LaTeX
$$$\\operatorname{exponent} G = \\max'\\langle \\operatorname{orderOf} g : g \\in G \\rangle$$$
Lean4
/-- If there exists an injective, multiplication-preserving map from `G` to `H`,
then the exponent of `G` divides the exponent of `H`.
-/
@[to_additive /-- If there exists an injective, addition-preserving map from `G` to `H`,
then the exponent of `G` divides the exponent of `H`. -/
]
theorem exponent_dvd_of_monoidHom (e : G →* H) (e_inj : Function.Injective e) : Monoid.exponent G ∣ Monoid.exponent H :=
exponent_dvd_of_forall_pow_eq_one fun g => e_inj (by rw [map_pow, pow_exponent_eq_one, map_one])
