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