coe_int_inv_mul_eq_one — Mathlib

English

The product of an integer and its inverse modulo n is 1, equivalently x^(-1) · x = 1.

Русский

Произведение числа и его обратного по модулю n равно 1; эквивалентно x^(-1) · x = 1.

LaTeX

$$$$ x \\cdot x^{-1} = 1 \\\\text{ in } \\mathbb{Z}/n\\mathbb{Z} $$$$

Lean4

theorem coe_int_inv_mul_eq_one {n : ℕ} {x : ℤ} (h : IsCoprime x n) : (x : ZMod n)⁻¹ * (x : ZMod n) = 1 := by
  rw [mul_comm, coe_int_mul_inv_eq_one h]

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