lean_workbook_plus_7445
ProvedLet be a set of eighteen (not necessarily distinct) integers. Prove that there exist two elements in whose difference is divisible by .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_7445 (S : Finset ℤ) (hS : S.card = 18) : ∃ a b, a ∈ S ∧ b ∈ S ∧ a - b ≡ 0 [ZMOD 17] := by sorry
Source