val_inv_mul — Mathlib

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]

Похожие утверждения