lean_workbook_plus_75763

Proved

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

Prove the Lemma: If $a \vert b$ and $a \vert c$ then $a \vert (mb - nc)$ where $a,b,c,m,n$ are integers.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_75763 (a b c m n : ℤ) (h₁ : a ∣ b) (h₂ : a ∣ c) : a ∣ (m * b - n * c)   :=  by sorry

Source