lean_workbook_plus_59081
ProvedProve inductively that for all .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_59081 (n : ℕ) (hn : 0 < n) : 6 ∣ 7^n - 1 := by sorry
Source
Prove inductively that for all .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_59081 (n : ℕ) (hn : 0 < n) : 6 ∣ 7^n - 1 := by sorry