lean_workbook_plus_70582
Proveddivides both and
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_70582 (p : ℕ) (hp : p ≡ 3 [ZMOD 4]) : 2 ∣ (p + 1) / 2 ∧ 2 ∣ (p - 1) := by sorry
Source
divides both and
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_70582 (p : ℕ) (hp : p ≡ 3 [ZMOD 4]) : 2 ∣ (p + 1) / 2 ∧ 2 ∣ (p - 1) := by sorry