Definition 1.8.1.32.  Let m ∈ +, n ∈ . We define:
m ∣ n  :⇔  ∃ x ∈  : m ⋅ x = n  ⇔  ∃! x ∈  : m ⋅ x = n
Equivalence.  No proof.
Remarks.

The constraint that m is nonzero is not really necessary but added for consistency with the definition of the set of divisors $Divisors.

References.