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 mul_inv_eq_gcd {n : ℕ} (a : ZMod n) : a * a⁻¹ = Nat.gcd a.val n :=
by
rcases n with - | n
· dsimp [ZMod] at a ⊢
calc
_ = a * Int.sign a := rfl
_ = a.natAbs := by rw [Int.mul_sign_self]
_ = a.natAbs.gcd 0 := by rw [Nat.gcd_zero_right]
·
calc
a * a⁻¹ = a * a⁻¹ + n.succ * Nat.gcdB (val a) n.succ := by rw [natCast_self, zero_mul, add_zero]
_ = ↑(↑a.val * Nat.gcdA (val a) n.succ + n.succ * Nat.gcdB (val a) n.succ) :=
by
push_cast
rw [natCast_zmod_val]
rfl
_ = Nat.gcd a.val n.succ := by rw [← Nat.gcd_eq_gcd_ab a.val n.succ]; rfl
