isOfFinOrder_pow — Mathlib

English

For any x in a monoid, x has finite periodic behavior under left-multiplication by x if and only if x^n = 1 for some n.

Русский

Для любого x в моноиде периодическое поведение левого умножения на x имеет место тогда и только тогда, когда существует n: x^n = 1.

LaTeX

$$$IsPeriodicPt( x \cdot )\, n \\ 1 \iff x^n = 1$$$

Lean4

@[to_additive (attr := simp)]
theorem isOfFinOrder_pow {n : ℕ} : IsOfFinOrder (a ^ n) ↔ IsOfFinOrder a ∨ n = 0 :=
  by
  rcases Decidable.eq_or_ne n 0 with rfl | hn
  · simp
  · exact ⟨fun h ↦ .inl <| h.of_pow hn, fun h ↦ (h.resolve_right hn).pow⟩

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