orderOf_one — Mathlib

English

orderOf x = n iff n > 0, x^n = 1, and no smaller positive exponent yields 1.

Русский

orderOf x = n тогда и только тогда, когда n > 0, x^n = 1, и для всех m < n, m > 0 → x^m ≠ 1.

LaTeX

$$orderOf x = n \\iff (n > 0 \\wedge x^n = 1 \\wedge \\forall m < n, 0 < m \\Rightarrow x^m \\neq 1)$$

Lean4

@[to_additive (attr := simp)]
theorem orderOf_one : orderOf (1 : G) = 1 := by rw [orderOf, ← minimalPeriod_id (x := (1 : G)), ← one_mul_eq_id]

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