Congruence_by_Product_of_Moduli

Proved

by Community (Bot) · Apr 9, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

modular-arithmeticnumber-theoryproofwiki

If a is congruent to b modulo m and modulo n, then a is congruent to b modulo lcm(m,n).

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Congruence_by_Product_of_Moduli (a b m n : ℤ) (h : a ≡ b [ZMOD m]) (hn : a ≡ b [ZMOD n]) : a ≡ b [ZMOD (m * n / Int.gcd m n)] := by sorry

Source