# The multiplicative monoid of natural numbers

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-09-28.

module elementary-number-theory.multiplicative-monoid-of-natural-numbers where

Imports
open import elementary-number-theory.equality-natural-numbers
open import elementary-number-theory.multiplication-natural-numbers

open import foundation.dependent-pair-types
open import foundation.universe-levels

open import group-theory.monoids
open import group-theory.semigroups


## Idea

The multiplicative monoid of natural numbers consists of natural numbers, and is equipped with the multiplication operation of the natural numbers as its multiplicative structure.

## Definitions

### The multiplicative semigroup of natural numbers

ℕ*-Semigroup : Semigroup lzero
pr1 ℕ*-Semigroup = ℕ-Set
pr1 (pr2 ℕ*-Semigroup) = mul-ℕ
pr2 (pr2 ℕ*-Semigroup) = associative-mul-ℕ


### The multiplicative monoid of natural numbers

ℕ*-Monoid : Monoid lzero
pr1 ℕ*-Monoid = ℕ*-Semigroup
pr1 (pr2 ℕ*-Monoid) = 1
pr1 (pr2 (pr2 ℕ*-Monoid)) = left-unit-law-mul-ℕ
pr2 (pr2 (pr2 ℕ*-Monoid)) = right-unit-law-mul-ℕ