# Reference manual / Extended toolkit / section numlaws

## Laws about Numbers in Z

Sam Valentine

Written September 1999.

Last updated September 1999.

 section numlaws parents numdefs, corelaws

This section contains the CADi version of some laws about numbers in the mathematical toolkit of Z.

### Prelude-based Laws

Those laws which depend solely on the definitions in the prelude are given in the file corelaws.z, which is a parent of this one.

### Theorems about the Natural Numbers

We could here state and prove various useful theorems about , both because of their usefulness, and to assist in proving the consistency of the definitions in numdefs.

The theorems would mainly be to the effect that is an Abelian monoid under _ * _, and _ * _ distributes through _ + _.

zeroTimesBEqZero ==

 ? b: 0 * b = 0

OneTimesBEqB ==

 ? b: 1 * b = b

TimesCommutes ==

 ? a, b: a * b = b * a

TimesDistributesThruPlus ==

 ? a, b, c: a * (b + c) = (a * b) + (a * c)

TimesClosed ==

 ? a, b: a * b

TimesAssociates ==

 ? a, b, c: (a * b) * c = a * (b * c)

TimesConstInjective ==

 ? a, b: ; c: 1 | a * c = b * c a = b

IT 18-Feb-2000