lean_workbook_plus_46320
ProvedWhen is odd:
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_46320 (n : ℕ) (h : n % 2 = 1) : (4:ℤ)^n + n^4 = (2^n + n^2)^2 - n^2 * 2^(n+1) := by sorry
Source
When is odd:
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_46320 (n : ℕ) (h : n % 2 = 1) : (4:ℤ)^n + n^4 = (2^n + n^2)^2 - n^2 * 2^(n+1) := by sorry