lean_workbook_plus_6643

Proved

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

If $x \equiv 0 \mod{ab}$ where $a$ and $b$ are coprime, then can we say, $x \equiv 0 \mod{a}$ and $x \equiv 0 \mod {b}$ ?

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_6643 (a b x : ℕ) (hab : Nat.Coprime a b) (h : x ≡ 0 [ZMOD a * b]) : x ≡ 0 [ZMOD a] ∧ x ≡ 0 [ZMOD b]   :=  by sorry

Source