orderOf_map_dvd — Mathlib

English

For monoid homomorphism ψ: G → H, ord(ψ(x)) divides ord(x).

Русский

Пусть ψ: G → H — гомоморфизм моноидов. Тогда ord(ψ(x)) делит ord(x).

LaTeX

$$$ \forall {G H} [Monoid G][Monoid H] (\psi : G \to_* H) (x : G), ord(\psi(x)) \mid ord(x)$$$

Lean4

@[to_additive]
theorem orderOf_map_dvd {H : Type*} [Monoid H] (ψ : G →* H) (x : G) : orderOf (ψ x) ∣ orderOf x :=
  by
  apply orderOf_dvd_of_pow_eq_one
  rw [← map_pow, pow_orderOf_eq_one]
  apply map_one

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