# Multiplication of natural numbers

```agda
module elementary-number-theory.multiplication-natural-numbers where
```

<details><summary>Imports</summary>

```agda
open import elementary-number-theory.addition-natural-numbers
open import elementary-number-theory.equality-natural-numbers
open import elementary-number-theory.natural-numbers

open import foundation.action-on-identifications-binary-functions
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.embeddings
open import foundation.identity-types
open import foundation.injective-maps
open import foundation.interchange-law
open import foundation.negated-equality
```

</details>

## Definition

### Multiplication

```agda
mul-ℕ :     
mul-ℕ 0 n = 0
mul-ℕ (succ-ℕ m) n = (mul-ℕ m n) +ℕ n

infixl 40 _*ℕ_
_*ℕ_ = mul-ℕ

mul-ℕ' :     
mul-ℕ' x y = mul-ℕ y x

ap-mul-ℕ :
  {x y x' y' : }  x  x'  y  y'  x *ℕ y  x' *ℕ y'
ap-mul-ℕ p q = ap-binary mul-ℕ p q

double-ℕ :   
double-ℕ x = 2 *ℕ x

triple-ℕ :   
triple-ℕ x = 3 *ℕ x
```

## Properties

```agda
abstract
  left-zero-law-mul-ℕ :
    (x : )  zero-ℕ *ℕ x  zero-ℕ
  left-zero-law-mul-ℕ x = refl

  right-zero-law-mul-ℕ :
    (x : )  x *ℕ zero-ℕ  zero-ℕ
  right-zero-law-mul-ℕ zero-ℕ = refl
  right-zero-law-mul-ℕ (succ-ℕ x) =
    ( right-unit-law-add-ℕ (x *ℕ zero-ℕ))  (right-zero-law-mul-ℕ x)

abstract
  right-unit-law-mul-ℕ :
    (x : )  x *ℕ 1  x
  right-unit-law-mul-ℕ zero-ℕ = refl
  right-unit-law-mul-ℕ (succ-ℕ x) = ap succ-ℕ (right-unit-law-mul-ℕ x)

  left-unit-law-mul-ℕ :
    (x : )  1 *ℕ x  x
  left-unit-law-mul-ℕ zero-ℕ = refl
  left-unit-law-mul-ℕ (succ-ℕ x) = ap succ-ℕ (left-unit-law-mul-ℕ x)

abstract
  left-successor-law-mul-ℕ :
    (x y : )  (succ-ℕ x) *ℕ y  (x *ℕ y) +ℕ y
  left-successor-law-mul-ℕ x y = refl

  right-successor-law-mul-ℕ :
    (x y : )  x *ℕ (succ-ℕ y)  x +ℕ (x *ℕ y)
  right-successor-law-mul-ℕ zero-ℕ y = refl
  right-successor-law-mul-ℕ (succ-ℕ x) y =
    ( ( ap  t  succ-ℕ (t +ℕ y)) (right-successor-law-mul-ℕ x y)) 
      ( ap succ-ℕ (associative-add-ℕ x (x *ℕ y) y))) 
    ( inv (left-successor-law-add-ℕ x ((x *ℕ y) +ℕ y)))

abstract
  commutative-mul-ℕ :
    (x y : )  x *ℕ y  y *ℕ x
  commutative-mul-ℕ zero-ℕ y = inv (right-zero-law-mul-ℕ y)
  commutative-mul-ℕ (succ-ℕ x) y =
    ( commutative-add-ℕ (x *ℕ y) y) 
    ( ( ap (y +ℕ_) (commutative-mul-ℕ x y)) 
      ( inv (right-successor-law-mul-ℕ y x)))

abstract
  left-distributive-mul-add-ℕ :
    (x y z : )  x *ℕ (y +ℕ z)  (x *ℕ y) +ℕ (x *ℕ z)
  left-distributive-mul-add-ℕ zero-ℕ y z = refl
  left-distributive-mul-add-ℕ (succ-ℕ x) y z =
    ( left-successor-law-mul-ℕ x (y +ℕ z)) 
    ( ( ap (_+ℕ (y +ℕ z)) (left-distributive-mul-add-ℕ x y z)) 
      ( ( associative-add-ℕ (x *ℕ y) (x *ℕ z) (y +ℕ z)) 
        ( ( ap
            ( ( x *ℕ y) +ℕ_)
            ( ( inv (associative-add-ℕ (x *ℕ z) y z)) 
              ( ( ap (_+ℕ z) (commutative-add-ℕ (x *ℕ z) y)) 
                ( associative-add-ℕ y (x *ℕ z) z)))) 
          ( inv (associative-add-ℕ (x *ℕ y) y ((x *ℕ z) +ℕ z))))))

abstract
  right-distributive-mul-add-ℕ :
    (x y z : )  (x +ℕ y) *ℕ z  (x *ℕ z) +ℕ (y *ℕ z)
  right-distributive-mul-add-ℕ x y z =
    ( commutative-mul-ℕ (x +ℕ y) z) 
    ( ( left-distributive-mul-add-ℕ z x y) 
      ( ( ap (_+ℕ (z *ℕ y)) (commutative-mul-ℕ z x)) 
        ( ap ((x *ℕ z) +ℕ_) (commutative-mul-ℕ z y))))

abstract
  associative-mul-ℕ :
    (x y z : )  (x *ℕ y) *ℕ z  x *ℕ (y *ℕ z)
  associative-mul-ℕ zero-ℕ y z = refl
  associative-mul-ℕ (succ-ℕ x) y z =
    ( right-distributive-mul-add-ℕ (x *ℕ y) y z) 
    ( ap (_+ℕ (y *ℕ z)) (associative-mul-ℕ x y z))

left-two-law-mul-ℕ :
  (x : )  2 *ℕ x  x +ℕ x
left-two-law-mul-ℕ x =
  ( left-successor-law-mul-ℕ 1 x) 
  ( ap (_+ℕ x) (left-unit-law-mul-ℕ x))

right-two-law-mul-ℕ :
  (x : )  x *ℕ 2  x +ℕ x
right-two-law-mul-ℕ x =
  ( right-successor-law-mul-ℕ x 1) 
  ( ap (x +ℕ_) (right-unit-law-mul-ℕ x))

interchange-law-mul-mul-ℕ : interchange-law mul-ℕ mul-ℕ
interchange-law-mul-mul-ℕ =
  interchange-law-commutative-and-associative
    mul-ℕ
    commutative-mul-ℕ
    associative-mul-ℕ

is-injective-right-mul-succ-ℕ :
  (k : )  is-injective (_*ℕ (succ-ℕ k))
is-injective-right-mul-succ-ℕ k {zero-ℕ} {zero-ℕ} p = refl
is-injective-right-mul-succ-ℕ k {succ-ℕ m} {succ-ℕ n} p =
  ap succ-ℕ
    ( is-injective-right-mul-succ-ℕ k {m} {n}
      ( is-injective-right-add-ℕ
        ( succ-ℕ k)
        ( ( inv (left-successor-law-mul-ℕ m (succ-ℕ k))) 
          ( ( p) 
            ( left-successor-law-mul-ℕ n (succ-ℕ k))))))

is-injective-right-mul-ℕ : (k : )  is-nonzero-ℕ k  is-injective (_*ℕ k)
is-injective-right-mul-ℕ k H p with
  is-successor-is-nonzero-ℕ H
... | pair l refl = is-injective-right-mul-succ-ℕ l p

is-injective-left-mul-succ-ℕ :
  (k : )  is-injective ((succ-ℕ k) *ℕ_)
is-injective-left-mul-succ-ℕ k {m} {n} p =
  is-injective-right-mul-succ-ℕ k
    ( ( commutative-mul-ℕ m (succ-ℕ k)) 
      ( p  commutative-mul-ℕ (succ-ℕ k) n))

is-injective-left-mul-ℕ :
  (k : )  is-nonzero-ℕ k  is-injective (k *ℕ_)
is-injective-left-mul-ℕ k H p with
  is-successor-is-nonzero-ℕ H
... | pair l refl = is-injective-left-mul-succ-ℕ l p

is-emb-left-mul-ℕ : (x : )  is-nonzero-ℕ x  is-emb (x *ℕ_)
is-emb-left-mul-ℕ x H =
  is-emb-is-injective is-set-ℕ (is-injective-left-mul-ℕ x H)

is-emb-right-mul-ℕ : (x : )  is-nonzero-ℕ x  is-emb (_*ℕ x)
is-emb-right-mul-ℕ x H =
  is-emb-is-injective is-set-ℕ (is-injective-right-mul-ℕ x H)

is-nonzero-mul-ℕ :
  (x y : )  is-nonzero-ℕ x  is-nonzero-ℕ y  is-nonzero-ℕ (x *ℕ y)
is-nonzero-mul-ℕ x y H K p =
  K (is-injective-left-mul-ℕ x H (p  (inv (right-zero-law-mul-ℕ x))))

is-nonzero-left-factor-mul-ℕ :
  (x y : )  is-nonzero-ℕ (x *ℕ y)  is-nonzero-ℕ x
is-nonzero-left-factor-mul-ℕ .zero-ℕ y H refl = H (left-zero-law-mul-ℕ y)

is-nonzero-right-factor-mul-ℕ :
  (x y : )  is-nonzero-ℕ (x *ℕ y)  is-nonzero-ℕ y
is-nonzero-right-factor-mul-ℕ x .zero-ℕ H refl = H (right-zero-law-mul-ℕ x)
```

We conclude that $y = 1$ if $(x+1)y = x+1$.

```agda
is-one-is-right-unit-mul-ℕ :
  (x y : )  (succ-ℕ x) *ℕ y  succ-ℕ x  is-one-ℕ y
is-one-is-right-unit-mul-ℕ x y p =
  is-injective-left-mul-succ-ℕ x (p  inv (right-unit-law-mul-ℕ (succ-ℕ x)))

is-one-is-left-unit-mul-ℕ :
  (x y : )  x *ℕ (succ-ℕ y)  succ-ℕ y  is-one-ℕ x
is-one-is-left-unit-mul-ℕ x y p =
  is-injective-right-mul-succ-ℕ y (p  inv (left-unit-law-mul-ℕ (succ-ℕ y)))

is-one-right-is-one-mul-ℕ :
  (x y : )  is-one-ℕ (x *ℕ y)  is-one-ℕ y
is-one-right-is-one-mul-ℕ zero-ℕ zero-ℕ p = p
is-one-right-is-one-mul-ℕ zero-ℕ (succ-ℕ y) ()
is-one-right-is-one-mul-ℕ (succ-ℕ x) zero-ℕ p =
  is-one-right-is-one-mul-ℕ x zero-ℕ p
is-one-right-is-one-mul-ℕ (succ-ℕ x) (succ-ℕ y) p =
  ap
    ( succ-ℕ)
    ( is-zero-right-is-zero-add-ℕ (x *ℕ (succ-ℕ y)) y
      ( is-injective-succ-ℕ p))

is-one-left-is-one-mul-ℕ :
  (x y : )  is-one-ℕ (x *ℕ y)  is-one-ℕ x
is-one-left-is-one-mul-ℕ x y p =
  is-one-right-is-one-mul-ℕ y x (commutative-mul-ℕ y x  p)

neq-mul-ℕ :
  (m n : )  succ-ℕ m  (succ-ℕ m *ℕ (succ-ℕ (succ-ℕ n)))
neq-mul-ℕ m n p =
  neq-add-ℕ
    ( succ-ℕ m)
    ( ( m *ℕ (succ-ℕ n)) +ℕ n)
    ( ( p) 
      ( ( right-successor-law-mul-ℕ (succ-ℕ m) (succ-ℕ n)) 
        ( ap ((succ-ℕ m) +ℕ_) (left-successor-law-mul-ℕ m (succ-ℕ n)))))
```