lean_workbook_plus_34191
ProvedFor show by induction that \n\na) \nb) \nc)
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_34191 (n : ℕ) (hn : 1 ≤ n) : 15 ∣ 2 ^ (4 * n) - 1 := by sorry
Source
For show by induction that \n\na) \nb) \nc)
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_34191 (n : ℕ) (hn : 1 ≤ n) : 15 ∣ 2 ^ (4 * n) - 1 := by sorry