English
If a and b are coprime, there exists y ∈ ℤ with a y ≡ 1 (mod b).
Русский
Если a и b взаимно просты, существует y ∈ ℤ such that a y ≡ 1 (mod b).
LaTeX
$$$\\forall {a,b \\in \\mathbb{N}}, \\ \\mathrm{gcd}(a,b)=1 \\Rightarrow \\exists y \\in \\mathbb{Z},\\ a y \\equiv 1 [ZMOD b].$$$
Lean4
theorem mod_coprime {a b : ℕ} (hab : Nat.Coprime a b) : ∃ y : ℤ, a * y ≡ 1 [ZMOD b] :=
⟨Nat.gcdA a b,
have hgcd : Nat.gcd a b = 1 := Nat.Coprime.gcd_eq_one hab
calc
↑a * Nat.gcdA a b ≡ ↑a * Nat.gcdA a b + ↑b * Nat.gcdB a b [ZMOD ↑b] :=
ModEq.symm <| modEq_add_fac _ <| ModEq.refl _
_ ≡ 1 [ZMOD ↑b] := by rw [← Nat.gcd_eq_gcd_ab, hgcd]; rfl⟩
