mul_val_inv — Mathlib

English

If m,n are coprime, then the product of m with the value of its inverse in ZMod n is 1: (m * (m⁻¹ : ZMod n).val) = 1.

Русский

Если m и n взаимно просты, то произведение m на значение обратного к m в ZMod n равно 1.

LaTeX

$$$ (m * (m^{-1} : ZMod n).val : ZMod n) = 1 \quad\text{whenever } \gcd(m,n)=1 $$$

Lean4

theorem mul_val_inv (hmn : m.Coprime n) : (m * (m⁻¹ : ZMod n).val : ZMod n) = 1 :=
  by
  obtain rfl | hn := eq_or_ne n 0
  · simp [m.coprime_zero_right.1 hmn]
  haveI : NeZero n := ⟨hn⟩
  rw [ZMod.natCast_zmod_val, ZMod.coe_mul_inv_eq_one _ hmn]

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