orderOf_dvd_iff_pow_eq_one — Mathlib

English

For any x in a monoid G and natural n, ord(x) divides n if and only if x^n = 1.

Русский

Для любого x в моноиде G и натурального n выполняется: ord(x) делит n тогда и только тогда, когда x^n = 1.

LaTeX

$$$ \forall G [Monoid G], \forall x : G, \forall n : \mathbb{N},\; ord(x) \mid n \;\leftrightarrow \; x^n = 1$$$

Lean4

@[to_additive]
theorem orderOf_dvd_iff_pow_eq_one {n : ℕ} : orderOf x ∣ n ↔ x ^ n = 1 :=
  ⟨fun h => by rw [← pow_mod_orderOf, Nat.mod_eq_zero_of_dvd h, _root_.pow_zero], orderOf_dvd_of_pow_eq_one⟩

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