Prove2Me

lean_workbook_plus_40528

Proved

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

prove that if a∣xa|x and a∣ya|y , then: \n a∣x+ya|x+y \n a∣x−ya|x-y \n a∣px+qya|px+qy for pp , qq integers

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_40528 : ∀ {a x y : ℤ} (h₁ : a ∣ x) (h₂ : a ∣ y), a ∣ x + y ∧ a ∣ x - y ∧ ∀ p q : ℤ, a ∣ p * x + q * y   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph