lean_workbook_plus_80258

Proved

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

If $n$ is odd, then $n^5$ and $n$ are both odd, which means $n^5-n$ is even. The same applies when $n$ is even. Hence, $n^5-n$ is divisible by $2$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_80258  (n : ℤ)
  (h₀ : Odd n) :
  2 ∣ (n^5 - n)   :=  by sorry

Source