Intersection_of_Congruence_Classes
Provedlowest-common-multiplemodulo-arithmeticproofwiki
If a ≡ b (mod m) and a ≡ b (mod n), then a ≡ b (mod lcm(m,n)).
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Intersection_of_Congruence_Classes (a b m n : ℤ) (hm : (a - b) % m = 0) (hn : (a - b) % n = 0) : (a - b) % Int.lcm m n = 0 := by sorry
Source