orderOf_a — Mathlib

English

For any i in ZMod(2n), order(a_i) = (2n)/gcd(2n,i).

Русский

Для любого i из ZMod(2n) порядок a_i равен (2n)/gcd(2n,i).

LaTeX

$$$\operatorname{orderOf}(a_i) = \dfrac{2n}{\gcd(2n,i)}$$$

Lean4

/-- If `0 < n`, then `a i` has order `(2 * n) / gcd (2 * n) i`.
-/
theorem orderOf_a [NeZero n] (i : ZMod (2 * n)) : orderOf (a i) = 2 * n / Nat.gcd (2 * n) i.val :=
  by
  conv_lhs => rw [← ZMod.natCast_zmod_val i]
  rw [← a_one_pow, orderOf_pow, orderOf_a_one]

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