a,b:
. a
b = 0 
a = 0 
b = 0a,b:. ab = 0 
a = 0 b = 0a,b:. a = 0 b = 0 ab = 0| Rank | Theorem | Name |
| 5 | a,b:. ab = 0 a = 0 b = 0 | [prod_zero_iff_factor_zero] |
| cites the following: | ||
| 4 | a,b:. ab = 0 a = 0 b = 0 | [int_entire] |
| 0 | a,b:. a = 0 b = 0 ab = 0 | [zero_ann_a] |