English
Let k, n be natural numbers with gcd(n, k) < k. Then there exists m ∈ ℕ such that n · m ≡ gcd(n, k) (mod k).
Русский
Пусть k, n — натуральные числа и gcd(n, k) < k. Тогда существует m ∈ ℕ такое, что n · m ≡ gcd(n, k) (mod k).
LaTeX
$$$$\\forall k,n \\in \\mathbb{N},\\; \\gcd(n,k) < k \\Rightarrow \\exists m \\in \\mathbb{N},\\; n m \\equiv \\gcd(n,k) \\pmod{k}.$$$$
Lean4
theorem exists_mul_emod_eq_gcd {k n : ℕ} (hk : gcd n k < k) : ∃ m, n * m % k = gcd n k :=
by
have hk' := Int.ofNat_ne_zero.2 (ne_of_gt (lt_of_le_of_lt (zero_le (gcd n k)) hk))
have key := congr_arg (fun (m : ℤ) => (m % k).toNat) (gcd_eq_gcd_ab n k)
simp only at key
rw [Int.add_mul_emod_self_left, ← Int.natCast_mod, Int.toNat_natCast, mod_eq_of_lt hk] at key
refine ⟨(n.gcdA k % k).toNat, Eq.trans (Int.ofNat.inj ?_) key.symm⟩
rw [Int.ofNat_eq_coe, Int.natCast_mod, Int.natCast_mul, Int.toNat_of_nonneg (Int.emod_nonneg _ hk'), Int.ofNat_eq_coe,
Int.toNat_of_nonneg (Int.emod_nonneg _ hk'), Int.mul_emod, Int.emod_emod, ← Int.mul_emod]
