coprime_of_mul_modEq_one — Mathlib

English

If a · b ≡ 1 (mod n) then a and n are coprime, i.e., gcd(a,n)=1.

Русский

Если a·b ≡ 1 (mod n), то gcd(a,n)=1.

LaTeX

$$$\\\\forall b\\\\in \\\\mathbb{N},\\\\ a \\\\in \\\\mathbb{N},\\\\ a \\\\cdot b \\\\equiv 1 \\\\pmod{n} \\\\Rightarrow \\\\gcd(a,n)=1$$$

Lean4

theorem coprime_of_mul_modEq_one (b : ℕ) {a n : ℕ} (h : a * b ≡ 1 [MOD n]) : a.Coprime n :=
  by
  obtain ⟨g, hh⟩ := Nat.gcd_dvd_right a n
  rw [Nat.coprime_iff_gcd_eq_one, ← Nat.dvd_one, ← Nat.modEq_zero_iff_dvd]
  calc
    1 ≡ a * b [MOD a.gcd n] := (hh ▸ h).symm.of_mul_right g
    _ ≡ 0 * b [MOD a.gcd n] := ((Nat.modEq_zero_iff_dvd.mpr (Nat.gcd_dvd_left _ _)).mul_right b)
    _ = 0 := by rw [zero_mul]

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