orderOf_eq_orderOf_iff — Mathlib

English

For any two elements x,y, ord(x) = ord(y) iff for all n, x^n = 1 ↔ y^n = 1.

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem orderOf_eq_orderOf_iff {H : Type*} [Monoid H] {y : H} :
    orderOf x = orderOf y ↔ ∀ n : ℕ, x ^ n = 1 ↔ y ^ n = 1 := by
  simp_rw [← isPeriodicPt_mul_iff_pow_eq_one, ← minimalPeriod_eq_minimalPeriod_iff, orderOf]

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