The natural numbers form a semiring

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

See note [foundational algebra order theory].

instance Nat.instAddMonoidWithOne : AddMonoidWithOne ℕ

Equations

• Nat.instAddMonoidWithOne = AddMonoidWithOne.mk Nat.instAddMonoidWithOne.proof_1 Nat.instAddMonoidWithOne.proof_2

instance Nat.instAddCommMonoidWithOne : AddCommMonoidWithOne ℕ

Equations

• Nat.instAddCommMonoidWithOne = AddCommMonoidWithOne.mk ⋯

instance Nat.instDistrib : Distrib ℕ

Equations

• Nat.instDistrib = Distrib.mk Nat.left_distrib Nat.right_distrib

instance Nat.instNonUnitalNonAssocSemiring : NonUnitalNonAssocSemiring ℕ

Equations

• Nat.instNonUnitalNonAssocSemiring = NonUnitalNonAssocSemiring.mk ⋯ ⋯ ⋯ ⋯

instance Nat.instNonUnitalSemiring : NonUnitalSemiring ℕ

Equations

• Nat.instNonUnitalSemiring = NonUnitalSemiring.mk Nat.instNonUnitalSemiring.proof_1

instance Nat.instNonAssocSemiring : NonAssocSemiring ℕ

Equations

• Nat.instNonAssocSemiring = NonAssocSemiring.mk Nat.instNonAssocSemiring.proof_1 Nat.instNonAssocSemiring.proof_2 Nat.instNonAssocSemiring.proof_3 Nat.instNonAssocSemiring.proof_4

instance Nat.instSemiring : Semiring ℕ

Equations

• Nat.instSemiring = Semiring.mk ⋯ ⋯ ⋯ ⋯ Monoid.npow Nat.instSemiring.proof_1 Nat.instSemiring.proof_2

instance Nat.instCommSemiring : CommSemiring ℕ

Equations

• Nat.instCommSemiring = CommSemiring.mk ⋯

theorem Nat.instCharZero : CharZero ℕ