coprime_mul_succ — Mathlib

English

If m − n divides a, then n·a + 1 and m·a + 1 are coprime.

Русский

Если m − n делит a, то числовые выражения n·a + 1 и m·a + 1 взаимно просты.

LaTeX

$$$\\text{If } m-n \\mid a, \\quad \\gcd(na+1, ma+1) = 1.$$$

Lean4

theorem coprime_mul_succ {n m a} (ha : m - n ∣ a) : Coprime (n * a + 1) (m * a + 1) :=
  Nat.coprime_of_dvd fun p pp hn hm =>
    by
    have : p ∣ (m - n) * a := by simpa [Nat.succ_sub_succ, ← Nat.mul_sub_right_distrib] using Nat.dvd_sub hm hn
    have : p ∣ a := by
      rcases (Nat.Prime.dvd_mul pp).mp this with (hp | hp)
      · exact Nat.dvd_trans hp ha
      · exact hp
    apply pp.ne_one
    simpa [Nat.add_sub_cancel_left] using Nat.dvd_sub hn (this.mul_left n)

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