lean_workbook_plus_59232
DisprovedShow that is divisible by for all .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_59232 (n:ℕ) (hn: 1 ≤ n) : 9 ∣ 9^n - 1 := by sorry
Source
Show that is divisible by for all .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_59232 (n:ℕ) (hn: 1 ≤ n) : 9 ∣ 9^n - 1 := by sorry