orderOf_eq_iff — Mathlib

English

In a Subsingleton monoid, every element has order 1.

Русский

В моноиде типа Subsingleton каждый элемент имеет порядок 1.

LaTeX

$$orderOf x = 1$$

Lean4

@[to_additive]
theorem orderOf_eq_iff {n} (h : 0 < n) : orderOf x = n ↔ x ^ n = 1 ∧ ∀ m, m < n → 0 < m → x ^ m ≠ 1 :=
  by
  simp_rw [Ne, ← isPeriodicPt_mul_iff_pow_eq_one, orderOf, minimalPeriod]
  split_ifs with h1
  ·
    classical
    rw [find_eq_iff]
    simp only [h, true_and]
    push_neg
    rfl
  · rw [iff_false_left h.ne]
    rintro ⟨h', -⟩
    exact h1 ⟨n, h, h'⟩

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