## Multiplication ∙

Natural number multiplication is defined recursively through the Peano axioms using the addition and successor operations. Natural number multiplication is used to construct integer multiplication. Integer multiplication is used to construct rational multiplication. Real multiplication is used to construct complex numbers. Since there are different versions of multiplication for each type of number, the properties are proved for each type of number. (The real numbers have not been constructed yet.)

### Properties

• Commutation: (= (* a b) (* b a)) /edit/peano_new/arithmetic/common/add_multiply_min.ghi/mulcom
• Association: (= (* (* a b) c) (* a (* b c))) /edit/peano_new/arithmetic/common/add_multiply_min.ghi/mulass
• Identity: (= (* a (1)) a) /edit/peano_new/arithmetic/common/add_multiply_min.ghi/mulid
• Zero Element: (= (* a (0)) (0)) /edit/peano_new/arithmetic/common/add_multiply.gh/mul0
• Distribution: (= (* a (+ b c)) (+ (* a b) (* a c))) /edit/peano_new/arithmetic/common/add_multiply_min.ghi/distr

### Multiplication Tables

• (* (2) (2)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/2times2, (* (2) (3)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/2times3, (* (2) (4)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/2times4, (* (2) (5)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/2times5, (* (2) (6)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/2times6, (* (2) (7)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/2times7, (* (2) (8)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/2times8, (* (2) (9)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/2times9
• (* (3) (2)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/3times2, (* (3) (3)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/3times3, (* (3) (4)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/3times4, (* (3) (5)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/3times5, (* (3) (6)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/3times6, (* (3) (7)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/3times7, (* (3) (8)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/3times8, (* (3) (9)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/3times9
• (* (4) (2)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/4times2, (* (4) (3)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/4times3, (* (4) (4)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/4times4, (* (4) (5)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/4times5, (* (4) (6)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/4times6, (* (4) (7)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/4times7, (* (4) (8)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/4times8, (* (4) (9)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/4times9
• (* (5) (2)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/5times2, (* (5) (3)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/5times3, (* (5) (4)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/5times4, (* (5) (5)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/5times5, (* (5) (6)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/5times6, (* (5) (7)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/5times7, (* (5) (8)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/5times8, (* (5) (9)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/5times9
• (* (6) (2)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/6times2, (* (6) (3)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/6times3, (* (6) (4)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/6times4, (* (6) (5)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/6times5, (* (6) (6)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/6times6, (* (6) (7)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/6times7, (* (6) (8)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/6times8, (* (6) (9)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/6times9
• (* (7) (2)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/7times2, (* (7) (3)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/7times3, (* (7) (4)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/7times4, (* (7) (5)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/7times5, (* (7) (6)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/7times6, (* (7) (7)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/7times7, (* (7) (8)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/7times8, (* (7) (9)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/7times9
• (* (8) (2)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/8times2, (* (8) (3)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/8times3, (* (8) (4)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/8times4, (* (8) (5)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/8times5, (* (8) (6)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/8times6, (* (8) (7)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/8times7, (* (8) (8)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/8times8, (* (8) (9)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/8times9
• (* (9) (2)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/9times2, (* (9) (3)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/9times3, (* (9) (4)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/9times4, (* (9) (5)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/9times5, (* (9) (6)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/9times6, (* (9) (7)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/9times7, (* (9) (8)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/9times8, (* (9) (9)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/9times9

### Examples

• (= (* (+ (10) (7)) (+ (10) (3))) (+ (* (2) (* (10) (10))) (+ (* (2) (10)) (1)))) /edit/peano/arithmetic.gh/multiplicationExample
• (= (* (+ (* (3) (* (10) (10))) (+ (* (8) (10)) (7))) (+ (* (2) (* (10) (10))) (3))) (+ (* (7) (* (10) (* (10) (* (10) (10))))) (+ (* (8) (* (10) (* (10) (10)))) (+ (* (5) (* (10) (10))) (+ (* (6) (10)) (1))))))/edit/peano/arithmetic.gh/multiplicationExample2
• (= (* (/ (1) (2)) (/ (4) (5))) (/ (2) (5))) /edit/peano_new/arithmetic/common/calculations/decimal.gh/multiplyFractions1
• (= (* (/ (+ (* (3) (10)) (6)) (5)) (/ (+ (* (6) (10)) (7)) (3))) (/ (+ (* (8) (* (10) (10))) (4)) (5))) /edit/peano_new/arithmetic/common/calculations/decimal.gh/multiplyFractions2