Law_of_Inverses_Modulo_Arithmetic
Provedmodular-arithmeticnumber-theoryproofwiki
For integers m and n, there exists an integer n' such that n * n' is congruent to gcd(m,n) modulo m.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Law_of_Inverses_Modulo_Arithmetic (m n : ℤ) : ∃ n' : ℤ, n * n' ≡ (Int.gcd m n : ℤ) [ZMOD m] := by sorry
Source