This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

The multiplicative monoid of natural numbers

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-ℕ