English
Given n ∈ ℕ, x ∈ ℕ and h : Nat.Coprime x n, the construction unitOfCoprime x h yields a unit of ZMod n with underlying value x and inverse x⁻¹, and coe_mul_inv_eq_one holds.
Русский
Для данного n, x и доказательства взаимной простоты x и n строится единица в ZMod n с основанием x и обратной x⁻¹, удовлетворяющая coe_mul_inv_eq_one.
LaTeX
$$$\text{unitOfCoprime}(n,x,h) \in (ZMod n)^{\times}, \text{ with underlying value } x \text{ and inverse } x^{-1}, \text{ and } coe\_mul\_inv\_eq\_one(x,h) $$$
Lean4
/-- `unitOfCoprime` makes an element of `(ZMod n)ˣ` given
a natural number `x` and a proof that `x` is coprime to `n` -/
def unitOfCoprime {n : ℕ} (x : ℕ) (h : Nat.Coprime x n) : (ZMod n)ˣ :=
⟨x, x⁻¹, coe_mul_inv_eq_one x h, by rw [mul_comm, coe_mul_inv_eq_one x h]⟩
