English
If gcd(x,n)=1, then x has a multiplicative inverse modulo n; equivalently x is a unit in ZMod n and x·x^(-1)=1.
Русский
Если gcd(x,n)=1, то x имеет мультипликативный обратный по модулю n; иначе x является единицей в ZMod n и x·x^(-1)=1.
LaTeX
$$$$ (\\text{IsCoprime } x\\; n) \\Rightarrow x \\cdot x^{-1} \\equiv 1 \\pmod{n} $$$$
Lean4
theorem coe_int_mul_inv_eq_one {n : ℕ} {x : ℤ} (h : IsCoprime x n) : (x : ZMod n) * (x : ZMod n)⁻¹ = 1 :=
by
by_cases hn : n = 0
· simp only [hn, Nat.cast_zero, isCoprime_zero_right] at h
rcases Int.isUnit_eq_one_or h with h | h <;> simp [h]
haveI : NeZero n := ⟨hn⟩
rw [← natCast_zmod_val x]
apply coe_mul_inv_eq_one
rwa [Int.isCoprime_iff_gcd_eq_one, ← Int.gcd_emod, ← val_intCast] at h
