exponent_dvd — Mathlib

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]

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