isOfFinOrder — Mathlib

English

The image of an element of finite order under a monoid homomorphism has finite order.

Русский

Образ элемента конечного порядка под одоморфизмом моноидов имеет конечный порядок.

LaTeX

$$IsOfFinOrder x \\Rightarrow IsOfFinOrder (f x)$$

Lean4

/-- The image of an element of finite order has finite order. -/
@[to_additive /-- The image of an element of finite additive order has finite additive order. -/
    ]
theorem isOfFinOrder [Monoid H] (f : G →* H) {x : G} (h : IsOfFinOrder x) : IsOfFinOrder <| f x :=
  isOfFinOrder_iff_pow_eq_one.mpr <| by
    obtain ⟨n, npos, hn⟩ := h.exists_pow_eq_one
    exact ⟨n, npos, by rw [← f.map_pow, hn, f.map_one]⟩

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