lean_workbook_plus_39585

Proved

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

Prove that if $x\equiv a\pmod m$ and $x \equiv a \pmod n$ then $x\equiv a \pmod{mn}$ , given that $m$ and $n$ are coprime.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_39585 (a m n x : ℕ) (hm : m > 0) (hn : n > 0) (hmn : Nat.Coprime m n) : x ≡ a [ZMOD m] ∧ x ≡ a [ZMOD n] → x ≡ a [ZMOD m * n]   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph