addOrderOf_coe' — Mathlib

English

If a ≠ 0, then addOrderOf(a : ZMod n) = n / gcd(n,a).

Русский

Если a ≠ 0, то addOrderOf(a : ZMod n) = n / gcd(n,a).

LaTeX

$$$ \operatorname{addOrderOf}(a : \mathrm{ZMod}\, n) = \dfrac{n}{\gcd(n,a)} $$$

Lean4

/-- This lemma works in the case in which `a ≠ 0`.  The version where
`ZMod n` is not infinite, i.e. `n ≠ 0`, is `addOrderOf_coe`. -/
@[simp]
theorem addOrderOf_coe' {a : ℕ} (n : ℕ) (a0 : a ≠ 0) : addOrderOf (a : ZMod n) = n / n.gcd a := by
  rw [← Nat.smul_one_eq_cast, addOrderOf_nsmul' _ a0, ZMod.addOrderOf_one]

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