chineseRemainder' — Mathlib

English

Given m, n and a, b with a ≡ b mod gcd(n,m), there exists a k such that k ≡ a mod n and k ≡ b mod m, with k < lcm(n,m).

Русский

Пусть m, n и a, b удовлетворяют a ≡ b (mod gcd(n,m)). Существует k такой, что k ≡ a (mod n) и k ≡ b (mod m), причем k < lcm(n,m).

LaTeX

$$$\\\\forall m,n\\\\, a\\\\, b \\\\in \\\\mathbb{N},\\\\ a \\\\equiv b \\\\pmod{\\\\gcd(n,m)} \\\\Rightarrow \\\\exists k \\\\in\\\\{0,\\\\dots, lcm(n,m)-1\\\\},\\\\ k \\\\equiv a \\\\pmod{n} \\\\land \\\\ k \\\\equiv b \\\\pmod{m}$$$

Lean4

/-- The natural number less than `lcm n m` congruent to `a` mod `n` and `b` mod `m` -/
def chineseRemainder' (h : a ≡ b [MOD gcd n m]) : { k // k ≡ a [MOD n] ∧ k ≡ b [MOD m] } :=
  if hn : n = 0 then
    ⟨a, by
      rw [hn, gcd_zero_left] at h; constructor
      · rfl
      · exact h⟩
  else
    if hm : m = 0 then
      ⟨b, by
        rw [hm, gcd_zero_right] at h; constructor
        · exact h.symm
        · rfl⟩
    else
      ⟨let (c, d) := xgcd n m;
        Int.toNat ((n * c * b + m * d * a) / gcd n m % lcm n m),
        by
        rw [xgcd_val]
        dsimp
        rw [modEq_iff_dvd, modEq_iff_dvd,
          Int.toNat_of_nonneg (Int.emod_nonneg _ (Int.natCast_ne_zero.2 (lcm_ne_zero hn hm)))]
        have hnonzero : (gcd n m : ℤ) ≠ 0 := by
          norm_cast
          rw [Nat.gcd_eq_zero_iff, not_and]
          exact fun _ => hm
        have hcoedvd : ∀ t, (gcd n m : ℤ) ∣ t * (b - a) := fun t => h.dvd.mul_left _
        have := gcd_eq_gcd_ab n m
        constructor <;> rw [Int.emod_def, ← sub_add] <;> refine Int.dvd_add ?_ (dvd_mul_of_dvd_left ?_ _) <;>
          try norm_cast
        · rw [← sub_eq_iff_eq_add'] at this
          rw [← this, Int.sub_mul, ← add_sub_assoc, add_comm, add_sub_assoc, ← Int.mul_sub, Int.add_ediv_of_dvd_left,
            Int.mul_ediv_cancel_left _ hnonzero, Int.mul_ediv_assoc _ h.dvd, ← sub_sub, sub_self, zero_sub, Int.dvd_neg,
            mul_assoc]
          · exact dvd_mul_right _ _
          norm_cast
          exact dvd_mul_right _ _
        · exact dvd_lcm_left n m
        · rw [← sub_eq_iff_eq_add] at this
          rw [← this, Int.sub_mul, sub_add, ← Int.mul_sub, Int.sub_ediv_of_dvd, Int.mul_ediv_cancel_left _ hnonzero,
            Int.mul_ediv_assoc _ h.dvd, ← sub_add, sub_self, zero_add, mul_assoc]
          · exact dvd_mul_right _ _
          · exact hcoedvd _
        · exact dvd_lcm_right n m⟩

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