English
The inverse on ZMod is defined by a piecewise map: inv(0,i) = Int.sign i, and inv(n+1,i) = Nat.gcdA(i.val, n+1).
Русский
Обратное на ZMod задаётся поразбивкой: inv(0,i) = Int.sign i, и inv(n+1,i) = Nat.gcdA(i.val, n+1).
LaTeX
$$$ inv : \forall n: \mathbb N, ZMod n \to ZMod n,\quad inv(0,i) = \mathrm{Int.sign}(i),\quad inv(n+1,i) = \mathrm{Nat.gcdA}(i.\text{val}, n+1). $$$
Lean4
/-- The inversion on `ZMod n`.
It is setup in such a way that `a * a⁻¹` is equal to `gcd a.val n`.
In particular, if `a` is coprime to `n`, and hence a unit, `a * a⁻¹ = 1`. -/
def inv : ∀ n : ℕ, ZMod n → ZMod n
| 0, i => Int.sign i
| n + 1, i => Nat.gcdA i.val (n + 1)
