lean_workbook_plus_78689
ProvedIf is odd, prove that
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_78689 (n : ℕ) (h : n % 2 = 1) : ¬ 3 ∣ (2^n - 1) := by sorry
Source
If is odd, prove that
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_78689 (n : ℕ) (h : n % 2 = 1) : ¬ 3 ∣ (2^n - 1) := by sorry