Divisibility Operator

Type: definition

The divisibility operator $a\mid b$ is defined for integers $a,b$.
It outputs TRUE if
\[
  b=ka
\]
for some integer $k$. Otherwise, it outputs FALSE.