English
If u is a unit in ZMod n, then the inverse of its image in ZMod n equals the image of its inverse as a unit.
Русский
Если u — единица в ZMod n, тогда обратное его образа в ZMod n равно образу его обратной единицы как элемента группы единиц.
LaTeX
$$$\bigl(u : \mathbb{Z}/n\mathbb{Z}\bigr)^{-1} = \bigl(u^{-1} : (\mathbb{Z}/n\mathbb{Z})^{\times}\bigr)$$$
Lean4
@[simp]
theorem inv_coe_unit {n : ℕ} (u : (ZMod n)ˣ) : (u : ZMod n)⁻¹ = (u⁻¹ : (ZMod n)ˣ) :=
by
have := congr_arg ((↑) : ℕ → ZMod n) (val_coe_unit_coprime u)
rw [← mul_inv_eq_gcd, Nat.cast_one] at this
let u' : (ZMod n)ˣ := ⟨u, (u : ZMod n)⁻¹, this, by rwa [mul_comm]⟩
have h : u = u' := by
apply Units.ext
rfl
rw [h]
rfl
