isOfFinOrder_coe — Mathlib

English

Let H be a submonoid of G and x ∈ H. Then x has finite order in H iff x has finite order in G.

Русский

Пусть H — подмоном G и x ∈ H. Тогда x имеет конечный порядок в H тогда и только тогда, когда x имеет конечный порядок в G.

LaTeX

$$$IsOfFinOrder (x : G) \\iff IsOfFinOrder x$$$

Lean4

/-- Elements of finite order are of finite order in submonoids. -/
@[to_additive /-- Elements of finite order are of finite order in submonoids. -/
    ]
theorem isOfFinOrder_coe {H : Submonoid G} {x : H} : IsOfFinOrder (x : G) ↔ IsOfFinOrder x :=
  by
  rw [isOfFinOrder_iff_pow_eq_one, isOfFinOrder_iff_pow_eq_one]
  norm_cast

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