English
If f: F M1 M2 is surjective, then exponent M2 divides exponent M1.
Русский
Пусть f: F M1 M2 сюрьективен; тогда экспонента M2 делит экспоненту M1.
LaTeX
$$$\text{exponent } M_2 \mid \text{exponent } M_1$$$
Lean4
/-- If `f : M₁ →⋆ M₂` is surjective, then the exponent of `M₂` divides the exponent of `M₁`. -/
@[to_additive]
theorem exponent_dvd {F M₁ M₂ : Type*} [Monoid M₁] [Monoid M₂] [FunLike F M₁ M₂] [MonoidHomClass F M₁ M₂] {f : F}
(hf : Function.Surjective f) : exponent M₂ ∣ exponent M₁ :=
by
refine Monoid.exponent_dvd_of_forall_pow_eq_one fun m₂ ↦ ?_
obtain ⟨m₁, rfl⟩ := hf m₂
rw [← map_pow, pow_exponent_eq_one, map_one]