coe_int_val_inv_mul — Mathlib

English

For coprime integer x and modulus n, the product of the cast x and its inverse equals 1 in ZMod n.

Русский

Для целого x, взаимно простого с n, произведение x и его обратного по модулю n равно 1 в ZMod n.

LaTeX

$$$$ (x \\text{ cast to } ZMod\\, n) \\cdot ((ZMod\\, n)^{-1} \\text{ of } x) = 1 $$$$

Lean4

theorem coe_int_val_inv_mul {n : ℕ} [NeZero n] {m : ℤ} (h : IsCoprime m n) : ((m⁻¹ : ZMod n).val : ZMod n) * m = 1 := by
  rw [mul_comm, coe_int_mul_val_inv h]

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