a,b:
. |a
b| = |a||b|a,b:. ab < 0 
a < 0 & b > 0 
a > 0 & b < 0a,b:. ab > 0 a > 0 & b > 0 a < 0 & b < 0| Rank | Theorem | Name |
| 5 | Thm* a,b:. |ab| = |a||b| | [absval_mul] |
| cites | ||
| 4 | Thm* a,b:. ab < 0 a < 0 & b > 0 a > 0 & b < 0 | [neg_mul_arg_bounds] |
| 3 | Thm* a,b:. ab > 0 a > 0 & b > 0 a < 0 & b < 0 | [pos_mul_arg_bounds] |