lean_workbook_plus_43729
ProvedProve that if and , then .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_43729 (p : ℕ) (hp1 : p ≡ 3 [ZMOD 5]) (hp2 : p ≡ 3 [ZMOD 8]) : 40 ∣ 13 * p + 1 := by sorry
Source
Prove that if and , then .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_43729 (p : ℕ) (hp1 : p ≡ 3 [ZMOD 5]) (hp2 : p ≡ 3 [ZMOD 8]) : 40 ∣ 13 * p + 1 := by sorry