Equivalent divisibility conditions over the integers
ProvedWorkbookTyped.plus_41584lean-workbookrepaired-variable-declarationssource-checked
Let and be integers. Show that divides if and only if it divides .
Declaration repair: Added explicit integer binders (a b : ℤ), as required by the source wording. The malformed platform declaration has undeclared variables; its inferred natural-number interpretation is not retained.
Source: InternLM Lean-Workbook, record lean_workbook_plus_41584 (Apache-2.0). Original malformed declaration. This record proves the corrected statement.
Preamble
import Mathlib
Formal statement
theorem WorkbookTyped.plus_41584 (a b : ℤ) : 29 ∣ (3 * a + 2 * b) ↔ 29 ∣ (11 * a + 17 * b) := by sorry
Source