isOfFinOrder — Mathlib

English

If x and y are conjugate, then finite order of x implies finite order of y.

Русский

Если x и y сопряжены, то конечный порядок x влечет конечный порядок y.

LaTeX

$$IsConj x y \\Rightarrow (IsOfFinOrder x \\Rightarrow IsOfFinOrder y)$$

Lean4

theorem isOfFinOrder (h : IsConj x y) : IsOfFinOrder x → IsOfFinOrder y :=
  by
  simp_rw [isOfFinOrder_iff_pow_eq_one]
  rintro ⟨n, n_gt_0, eq'⟩
  exact ⟨n, n_gt_0, by rw [← isConj_one_right, ← eq']; exact h.pow n⟩

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