English
If z ≡ a (mod n) and z ≡ b (mod m) for coprime n,m, then z ≡ ChineseRemainder(co) a b (mod nm).
Русский
Если z ≡ a (mod n) и z ≡ b (mod m) при взаимно простых n,m, то z ≡ ChineseRemainder(co) a b (mod nm).
LaTeX
$$$\\\\forall n,m \\\\in \\\\mathbb{N},\\\\ n \\\\perp m \\\\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_lt_mul (co : n.Coprime m) (a b : ℕ) (hn : n ≠ 0) (hm : m ≠ 0) :
↑(chineseRemainder co a b) < n * m :=
lt_of_lt_of_le (chineseRemainder'_lt_lcm _ hn hm) (le_of_eq co.lcm_eq_mul)
