lean_workbook_plus_54976
Proved.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_54976 (p : ℕ) (hp : p ≡ 1 [ZMOD 6]) : ∃ m : ℕ, p = 6*m + 1 := by sorry
Source
.
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_54976 (p : ℕ) (hp : p ≡ 1 [ZMOD 6]) : ∃ m : ℕ, p = 6*m + 1 := by sorry