isOfFinOrder_iff_isUnit — Mathlib

English

For a monoid G with finite group of units, an element has finite order iff it is a unit.

Русский

Для моноида G с конечной группой единиц элемент имеет конечный порядок тогда и только тогда, когда он является единицей.

LaTeX

$$[Monoid G] [Finite Gˣ] {x : G} : IsOfFinOrder x ↔ IsUnit x$$

Lean4

theorem isOfFinOrder_iff_isUnit [Monoid G] [Finite Gˣ] {x : G} : IsOfFinOrder x ↔ IsUnit x :=
  by
  use IsOfFinOrder.isUnit
  rintro ⟨u, rfl⟩
  rw [Units.isOfFinOrder_val]
  apply isOfFinOrder_of_finite

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