English
Let a,b,m,n be integers with m.natAbs coprime to n.natAbs. Then a ≡ b [ZMOD m] ∧ a ≡ b [ZMOD n] iff a ≡ b [ZMOD m n].
Русский
Пусть a,b,m,n целые, перестановочная взаимно простота m.natAbs и n.natAbs. Тогда a ≡ b [ZMOD m] и a ≡ b [ZMOD n] эквивалентно a ≡ b [ZMOD m n].
LaTeX
$$$\\forall a,b,m,n \\in \\mathbb{Z},\\, m{\\operatorname{natAbs}}.\\mathrm{Coprime}\\ n{\\operatorname{natAbs}} \\Rightarrow (a \\equiv b [ZMOD m] \\land a \\equiv b [ZMOD n]) \\iff a \\equiv b [ZMOD m n].$$$
Lean4
theorem modEq_and_modEq_iff_modEq_mul {a b m n : ℤ} (hmn : m.natAbs.Coprime n.natAbs) :
a ≡ b [ZMOD m] ∧ a ≡ b [ZMOD n] ↔ a ≡ b [ZMOD m * n] :=
⟨fun h => by
rw [modEq_iff_dvd, modEq_iff_dvd] at h
rw [modEq_iff_dvd, ← natAbs_dvd, ← dvd_natAbs, natCast_dvd_natCast, natAbs_mul]
refine hmn.mul_dvd_of_dvd_of_dvd ?_ ?_ <;> rw [← natCast_dvd_natCast, natAbs_dvd, dvd_natAbs] <;> tauto, fun h =>
⟨h.of_mul_right _, h.of_mul_left _⟩⟩
