The natural numbers form a semiring

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

See note [foundational algebra order theory].

Instances

instance Nat.instCommSemiring : CommSemiring ℕ

Equations

• Nat.instCommSemiring = let __spread.0 := Nat.instCommMonoid; CommSemiring.mk ⋯

instance Nat.instCancelCommMonoidWithZero : CancelCommMonoidWithZero ℕ

Equations

• Nat.instCancelCommMonoidWithZero = let __spread.0 := inferInstance; CancelCommMonoidWithZero.mk

instance Nat.instMulDivCancelClass : MulDivCancelClass ℕ

Equations

• Nat.instMulDivCancelClass = ⋯

Extra instances to short-circuit type class resolution

These also prevent non-computable instances being used to construct these instances non-computably.

instance Nat.instAddCommMonoidWithOne : AddCommMonoidWithOne ℕ

Equations

• Nat.instAddCommMonoidWithOne = inferInstance

instance Nat.instDistrib : Distrib ℕ

Equations

• Nat.instDistrib = inferInstance

instance Nat.instSemiring : Semiring ℕ

Equations

• Nat.instSemiring = inferInstance