Documentation

Mathlib.Algebra.GroupWithZero.Nat

The natural numbers form a cancellative CommMonoidWithZero #

This file contains the CommMonoidWithZero and IsCancelMulZero instances on the natural numbers.

See note [foundational algebra order theory].

source
🔸 coverage
instance Nat.instMulZeroClass :
MulZeroClass ℕ
Equations
    source
    🔸 coverage
    instance Nat.instSemigroupWithZero :
    SemigroupWithZero ℕ
    Equations
      source
      🔸 coverage
      instance Nat.instMonoidWithZero :
      MonoidWithZero ℕ
      Equations
        source
        🔸 coverage
        instance Nat.instCommMonoidWithZero :
        CommMonoidWithZero ℕ
        Equations
          source
          📐 coverage
          instance Nat.instIsCancelMulZero :
          IsCancelMulZero ℕ
          source
          📐 coverage
          instance Nat.instMulDivCancelClass :
          MulDivCancelClass ℕ
          source
          🔸 coverage
          instance Nat.instMulZeroOneClass :
          MulZeroOneClass ℕ
          Equations