English
There is a canonical unit of ZMod m associated with an integer n that is coprime to m, with its value and inverse given by n and n^(-1).
Русский
Существует каноническая единица ZMod m, связанная с целым n, взаимно простым с m, с теми значениями и обратным, равными n и n^(-1).
LaTeX
$$$$ {m : \\mathbb{N}} \\; (n : \\mathbb{Z}) \\; (h : \\mathrm{IsCoprime}\\, n\, (m : \\mathbb{Z})) \\to (\\mathrm{ZMod}\\, m)^{\\times} $$$$
Lean4
/-- The unit of `ZMod m` associated with an integer prime to `n`. -/
def unitOfIsCoprime {m : ℕ} (n : ℤ) (h : IsCoprime n (m : ℤ)) : (ZMod m)ˣ
where
val := n
inv := n⁻¹
val_inv := coe_int_mul_inv_eq_one h
inv_val := coe_int_inv_mul_eq_one h
