lean_workbook_plus_26581
ProvedWhen , it is .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_26581 : ∀ m : ℕ, 1 ≤ m → 3^(2^m) - 1 = (3^(2^(m-1)) - 1) * (3^(2^(m-1)) + 1) := by sorry
Source
When , it is .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_26581 : ∀ m : ℕ, 1 ≤ m → 3^(2^m) - 1 = (3^(2^(m-1)) - 1) * (3^(2^(m-1)) + 1) := by sorry