Chinese_Remainder_Theorem
Provedmodular-arithmeticnumber-theoryproofwiki
Let a, b, r, s be integers with r and s coprime. Then there exists x such that x is congruent to a (mod r) and x is congruent to b (mod s).
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Chinese_Remainder_Theorem (a b r s : ℤ) (hcoprime : IsCoprime r s) : ∃ x : ℤ, x ≡ a [ZMOD r] ∧ x ≡ b [ZMOD s] := by sorry
Source