def IsPerfectDifferenceSet (D : Set ℕ) (n : ℕ) : Prop

A perfect difference set modulo n is a set D such that the map (a, b) ↦ a - b from D.offDiag to {x : ZMod n | x ≠ 0} is a bijection.

Equations

• IsPerfectDifferenceSet D n = Set.BijOn (fun (x : ℕ × ℕ) => match x with | (a, b) => ↑a - ↑b) D.offDiag {x : ZMod n | x ≠ 0}