English
If m,n are coprime, then the inverse value times m equals 1 in ZMod n: ((m⁻¹ : ZMod n).val * m) = 1.
Русский
Если m и n взаимно просты, то значение обратного к m, умноженное на m, равно 1 в ZMod n.
LaTeX
$$$ ((m^{-1} : ZMod n).val * m : ZMod n) = 1 \quad\text{for } \gcd(m,n)=1 $$$
Lean4
theorem val_inv_mul (hmn : m.Coprime n) : ((m⁻¹ : ZMod n).val * m : ZMod n) = 1 := by rw [mul_comm, mul_val_inv hmn]