Theorems · Theorem · group theory

MonoidHom.exponent_dvd

∀ {F : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [inst : Monoid M₁] [inst_1 : Monoid M₂] [inst_2 : FunLike F M₁ M₂]
  [MonoidHomClass F M₁ M₂] {f : F}, Function.Surjective ⇑f → Monoid.exponent M₂ ∣ Monoid.exponent M₁

If f : M₁ →⋆ M₂ is surjective, then the exponent of M₂ divides the exponent of M₁.

Defined in

Mathlib.GroupTheory.Exponent

Cited by

5 results in Mathlib

Foundations

Depth 76 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MonoidMonoidFunLikeMonoidHomClass