lean_workbook_plus_69273

Proved

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

Demonstrate the rule: $a | (am+b)^n - b^n$ for $a, m, b, n \in \mathbb{N}$ and $0 \le b < a$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_69273 (a m b n : ℕ) (h₀ : 0 < n) (h₁ : 0 < a) (h₂ : 0 < b) (h₃ : b < a) :
  a ∣ (a*m + b)^n - b^n   :=  by sorry

Source