lean_workbook_plus_33417

$x \equiv y \bmod z$ is true if and only if $x - y$ is divisible by $z$ (or, actually, if you still want to think about it in terms of remainders, if $x$ and $y$ both give the same remainder upon division by $z$ ). For example, $15 \equiv 35 \bmod 20$ because $15 - 35 = -20$ , which is divisible by $20$ .