orderOf_pow_dvd — Mathlib

English

For any x in a monoid G and natural n, the order of x^n divides the order of x.

Русский

Для любого x в моноиде G и натурального n порядок x^n делит порядок x.

LaTeX

$$$ \forall G [Monoid G], \forall x : G, \forall n : \mathbb{N},\; ord(x^n) \mid ord(x)$$$

Lean4

@[to_additive addOrderOf_smul_dvd]
theorem orderOf_pow_dvd (n : ℕ) : orderOf (x ^ n) ∣ orderOf x := by
  rw [orderOf_dvd_iff_pow_eq_one, pow_right_comm, pow_orderOf_eq_one, one_pow]

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