exists_mul_emod_eq_one_of_coprime

English

Let k, n ∈ ℕ with gcd(n, k) = 1 and k > 1. Then there exists an m ∈ ℕ such that n m ≡ 1 (mod k).

Русский

Пусть k, n ∈ ℕ, gcd(n, k) = 1 и k > 1. Тогда существует m ∈ ℕ такое, что n m ≡ 1 (mod k).

LaTeX

$$$$\\forall k,n \\in \\mathbb{N},\\; \\gcd(n,k)=1 \\wedge 1

Lean4

theorem exists_mul_emod_eq_one_of_coprime {k n : ℕ} (hkn : Coprime n k) (hk : 1 < k) : ∃ m, n * m % k = 1 :=
  Exists.recOn (exists_mul_emod_eq_gcd (lt_of_le_of_lt (le_of_eq hkn) hk)) fun m hm ↦ ⟨m, hm.trans hkn⟩

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