The natural numbers form a semiring #
This file contains the commutative semiring instance on the natural numbers.
See note [foundational algebra order theory].
Instances #
Equations
- Nat.instCommSemiring = let __spread.0 := Nat.instCommMonoid; CommSemiring.mk ⋯
Equations
- Nat.instCancelCommMonoidWithZero = let __spread.0 := inferInstance; CancelCommMonoidWithZero.mk
Extra instances to short-circuit type class resolution #
These also prevent non-computable instances being used to construct these instances non-computably.
Equations
- Nat.instAddCommMonoidWithOne = inferInstance