English
For coprime m,n, a ≡ b mod m and a ≡ b mod n if and only if a ≡ b mod (m n).
Русский
Для взаимно простых m,n верно: a ≡ b (mod m) и a ≡ b (mod n) тогда и только тогда, когда a ≡ b (mod mn).
LaTeX
$$$\\\\forall a,b,m,n \\\\in \\\\mathbb{N},\\\\ hmn : m \\\\perp n \\\\Rightarrow \\\\bigl(a \\\\equiv b \\\\pmod{m} \\\\land \\\\ a \\\\equiv b \\\\pmod{n}\\bigr) \\\\Leftrightarrow a \\\\equiv b \\\\pmod{m n}$$$
Lean4
theorem modEq_and_modEq_iff_modEq_mul {a b m n : ℕ} (hmn : m.Coprime n) :
a ≡ b [MOD m] ∧ a ≡ b [MOD n] ↔ a ≡ b [MOD m * n] :=
⟨fun h =>
by
rw [Nat.modEq_iff_dvd, Nat.modEq_iff_dvd, ← Int.dvd_natAbs, Int.natCast_dvd_natCast, ← Int.dvd_natAbs,
Int.natCast_dvd_natCast] at h
rw [Nat.modEq_iff_dvd, ← Int.dvd_natAbs, Int.natCast_dvd_natCast]
exact hmn.mul_dvd_of_dvd_of_dvd h.1 h.2, fun h => ⟨h.of_mul_right _, h.of_mul_left _⟩⟩
