lean_workbook_plus_67313

Proved

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

Given that for any odd integer, either $n+1$ or $n-1$ is divisible by 4, prove that $(n+1)(n-1)$ is divisible by 4

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_67313 : ∀ n : ℤ, n % 2 = 1 → 4 ∣ (n + 1) * (n - 1)   :=  by sorry

Source