a:
, b:
. (a rem -b) = (a rem b)a:
, n:{...-1}. (a rem n) = (a rem -n)a:{...0}, n:
. (a rem n) = -((-a) rem n)a:{...0}, n:{...-1}. (a rem n) = -((-a) rem -n)| Rank | Theorem | Name |
| 6 |
Thm* a:, b:. (a rem -b) = (a rem b) | [rem_sym] |
| cites | ||
| 5 |
Thm* a:, n:{...-1}. (a rem n) = (a rem -n) | [rem_4_to_1] |
| 5 |
Thm* a:{...0}, n:. (a rem n) = -((-a) rem n) | [rem_2_to_1] |
| 5 |
Thm* a:{...0}, n:{...-1}. (a rem n) = -((-a) rem -n) | [rem_3_to_1] |