lean_workbook_plus_20231
ProvedProve that if , the only such prime is .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_20231 (p : ℕ) (hp : p.Prime) (h : p ≡ 0 [ZMOD 3]) : p = 3 := by sorry
Source
Prove that if , the only such prime is .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_20231 (p : ℕ) (hp : p.Prime) (h : p ≡ 0 [ZMOD 3]) : p = 3 := by sorry