lean_workbook_plus_23949

Proved

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

Prove that if $a \equiv b \pmod m$ and $n | m$ , then $a \equiv b \pmod n$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_23949 (a b m n : ℤ) (h₁ : a ≡ b [ZMOD m]) (h₂ : n ∣ m) : a ≡ b [ZMOD n]   :=  by sorry

Source