lean_workbook_plus_59953

Proved

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

Let $a,b \in \mathbb{Z}$ and $m,n \in \mathbb{N}$ . Show that if $a \equiv b (mod n)$ and if $m|n$ , then $a \equiv b (mod m)$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_59953 (a b : ℤ) (m n : ℕ) (h1 : a ≡ b [ZMOD n]) (h2 : m ∣ n) : a ≡ b [ZMOD m]   :=  by sorry

Source