The multiplicative monoid of natural numbers

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-09-28.
Last modified on 2023-10-22.

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

Recent changes