lean_workbook_plus_850

Proved

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

Now let $p=2$ . A necessary condition for $a^{2^n}- 1$ to be even is $a$ to be odd. Conversely, if $a$ is odd, then all factors (which are $n+1$ in amount) are even, so the whole product is divisible by $2^{n+1}$ (and in particular, by $2^n$ ).

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_850  (a n : ℕ)
  (h₀ : Odd a)
  : Even (a^(2^n) - 1)   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph