coe_mul_inv_eq_one — Mathlib

English

For every a ∈ ZMod n, a · a⁻¹ equals gcd(a.val, n) in ZMod n.

Русский

Для каждого a ∈ ZMod n, a · a⁻¹ равняется gcd(a.val, n) в ZMod n.

LaTeX

$$$ a \cdot a^{-1} = \gcd(a.\text{val}, n) \text{ (in ZMod } n\text{)} $$$

Lean4

theorem coe_mul_inv_eq_one {n : ℕ} (x : ℕ) (h : Nat.Coprime x n) : ((x : ZMod n) * (x : ZMod n)⁻¹) = 1 :=
  by
  rw [Nat.Coprime, Nat.gcd_comm, Nat.gcd_rec] at h
  rw [mul_inv_eq_gcd, val_natCast, h, Nat.cast_one]

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