orderOf_r — Mathlib

English

Let n > 0 and i ∈ ZMod n. The order of r i equals n divided by gcd(n, i).

Русский

Пусть n > 0 и i ∈ ZMod n. Порядок элемента r i равен n / gcd(n, i).

LaTeX

$$\operatorname{order}(r i) = \dfrac{n}{\gcd(n, i)}$$

Lean4

/-- If `0 < n`, then `i : ZMod n` has order `n / gcd n i`.
-/
theorem orderOf_r [NeZero n] (i : ZMod n) : orderOf (r i) = n / Nat.gcd n i.val :=
  by
  conv_lhs => rw [← ZMod.natCast_zmod_val i]
  rw [← r_one_pow, orderOf_pow, orderOf_r_one]

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