Divisor

DEF-DIV. Divisor.

Let $n$, $m\in\N$. We say

• $n$ divides $m$,
• or $n$ is a divisor / factor of $m$,
• or $m$ is a multiple of $n$,
• or $m$ is divisible by $n$,

written $n\divides m$, if there exists $k\in\N$ such that $m=kn$.

PROP-DIV-ZERO.

1. $0\divides n$ for all $n\in\N$.
2. $n\not\divides 0$ for all $n\in\N^+$.