b:
. b | 1 
b = 
1a:
, b:
. a | b a
ba:. 0 | a a = 0a,b:. a | b 
-a | b| Rank | Theorem | Name |
| 2 | b:. b | 1 b = 1 | [only_pm_one_divs_one] |
| cites the following: | ||
| 1 | a:, b:. a | b ab | [divisors_bound] |
| 0 | a:. 0 | a a = 0 | [zero_divs_only_zero] |
| 0 | a,b:. a | b -a | b | [divides_invar_1] |