English
If z ≡ a mod n and z ≡ b mod m, then z ≡ ChineseRemainder(n,m;a,b) mod nm, when gcd(n,m)=1.
Русский
Если z ≡ a mod n и z ≡ b mod m, то z ≡ ChineseRemainder(n,m;a,b) mod nm при gcd(n,m)=1.
LaTeX
$$$\\\\forall n,m \\\\in \\\\mathbb{N},\\\\ gcd(n,m)=1 \\\\Rightarrow \\\\forall a,b,z \\\\in \\\\mathbb{N},\\\\ z \\\\equiv a \\\\pmod{n} \\\\land \\\\ z \\\\equiv b \\\\pmod{m} \\\\Rightarrow \\\\ z \\\\equiv \\text{ChineseRemainder}(n,m;a,b) \\\\pmod{nm}$$$
Lean4
theorem chineseRemainder_modEq_unique (co : n.Coprime m) {a b z} (hzan : z ≡ a [MOD n]) (hzbm : z ≡ b [MOD m]) :
z ≡ chineseRemainder co a b [MOD n * m] := by
simpa [Nat.Coprime.lcm_eq_mul co] using
mod_lcm (hzan.trans ((chineseRemainder co a b).prop.1).symm) (hzbm.trans ((chineseRemainder co a b).prop.2).symm)
