pow — Mathlib

English

If IsOfFinOrder a holds, then IsOfFinOrder a^n holds for any n.

Русский

Если a имеет конечный порядок, то и a^n имеет конечный порядок для любого n.

LaTeX

$$$IsOfFinOrder(a) \Rightarrow IsOfFinOrder(a^n)$$$

Lean4

@[to_additive]
theorem pow {n : ℕ} : IsOfFinOrder a → IsOfFinOrder (a ^ n) :=
  by
  simp_rw [isOfFinOrder_iff_pow_eq_one]
  rintro ⟨m, hm, ha⟩
  exact ⟨m, hm, by simp [pow_right_comm _ n, ha]⟩

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