Documentation

Mathlib.Algebra.Ring.Nat

The natural numbers form a semiring #

This file contains the commutative semiring instance on the natural numbers.

See note [foundational algebra order theory].

source
🔸 coverage
@[implicit_reducible]
instance Nat.instAddMonoidWithOne :
AddMonoidWithOne ℕ
source
🔸 coverage
@[implicit_reducible]
instance Nat.instAddCommMonoidWithOne :
AddCommMonoidWithOne ℕ
source
🔸 coverage
@[implicit_reducible]
instance Nat.instDistrib :
Distrib ℕ
source
🔸 coverage
@[implicit_reducible]
instance Nat.instNonUnitalNonAssocSemiring :
NonUnitalNonAssocSemiring ℕ
source
🔸 coverage
@[implicit_reducible]
instance Nat.instNonUnitalSemiring :
NonUnitalSemiring ℕ
source
🔸 coverage
@[implicit_reducible]
instance Nat.instNonAssocSemiring :
NonAssocSemiring ℕ
source
🔸 coverage
@[implicit_reducible]
instance Nat.instSemiring :
Semiring ℕ
source
🔸 coverage
@[implicit_reducible]
instance Nat.instCommSemiring :
CommSemiring ℕ
source
📐 coverage
instance Nat.instCharZero :
CharZero ℕ
source
📐 coverage
instance Nat.instIsDomain :
IsDomain ℕ