Skip to content
Definition·D060

Multiplication of integers

Multiply integers by the cross formula on representative pairs, mirroring how (a minus b) times (c minus d) expands.

For , write and with , and define (using natural-number addition and multiplication). This does not depend on the choice of representatives, so is a well-defined binary operation on .
In words
To multiply two integers, pick representative pairs and cross-multiply and add according to the rule for (a minus b) times (c minus d), taking the class of the result.
Rests onA02
Never needed: F02 · F03 · F04 · F05 · F06 · F08 · F09 · F10 · F11 · F12 · F13 · F14 · A01 · A03 · A04 · A05 · A06 · A07 · A08 (computed from the citation graph, not asserted).

Remarks

By L44, the result does not depend on the representatives chosen. The formula mirrors , expressed additively since subtraction is not directly available on . Under the embedding, (L46), so this extends multiplication on .

Used by