The multiplicative monoid of nonnegative rational numbers

Content created by Louis Wasserman.

Created on 2025-10-19.
Last modified on 2025-10-19.

{-# OPTIONS --lossy-unification #-}

module elementary-number-theory.multiplicative-monoid-of-nonnegative-rational-numbers where
Imports 
open import elementary-number-theory.multiplication-nonnegative-rational-numbers
open import elementary-number-theory.multiplicative-monoid-of-rational-numbers
open import elementary-number-theory.nonnegative-rational-numbers

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

open import group-theory.commutative-monoids
open import group-theory.monoids
open import group-theory.submonoids-commutative-monoids

Idea

The type of nonnegative rational numbers equipped with multiplication is a commutative monoid with unit one-ℚ⁰⁺.

Definitions

The multiplicative commutative monoid of nonnegative rational numbers

nonnegative-submonoid-commutative-monoid-mul-ℚ :
  Commutative-Submonoid lzero commutative-monoid-mul-ℚ
nonnegative-submonoid-commutative-monoid-mul-ℚ =
  ( is-nonnegative-prop-ℚ ,
    is-nonnegative-one-ℚ ,
    λ _ _ → is-nonnegative-mul-ℚ)

commutative-monoid-mul-ℚ⁰⁺ : Commutative-Monoid lzero
commutative-monoid-mul-ℚ⁰⁺ =
  commutative-monoid-Commutative-Submonoid
    ( commutative-monoid-mul-ℚ)
    ( nonnegative-submonoid-commutative-monoid-mul-ℚ)

monoid-mul-ℚ⁰⁺ : Monoid lzero
monoid-mul-ℚ⁰⁺ = monoid-Commutative-Monoid commutative-monoid-mul-ℚ⁰⁺

Recent changes