lean_workbook_plus_3370
ProvedProve that if is a prime number, then divides .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_3370 (p : ℕ) (hp : p.Prime) (h2 : p > 2) : 2 ∣ p - 1 := by sorry
Source
Prove that if is a prime number, then divides .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_3370 (p : ℕ) (hp : p.Prime) (h2 : p > 2) : 2 ∣ p - 1 := by sorry