The natural numbers form a semiring

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

See note [foundational algebra order theory].

@[implicit_reducible]

instance Nat.instAddMonoidWithOne : AddMonoidWithOne ℕ

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Nat.instAddCommMonoidWithOne : AddCommMonoidWithOne ℕ

Equations

• Nat.instAddCommMonoidWithOne = { toAddMonoidWithOne := Nat.instAddMonoidWithOne, add_comm := ⋯ }

@[implicit_reducible]

instance Nat.instDistrib : Distrib ℕ

Equations

• Nat.instDistrib = { toMul := instMulNat, toAdd := instAddNat, left_distrib := Nat.left_distrib, right_distrib := Nat.right_distrib }

@[implicit_reducible]

instance Nat.instNonUnitalNonAssocSemiring : NonUnitalNonAssocSemiring ℕ

Equations

• Nat.instNonUnitalNonAssocSemiring = { toAddCommMonoid := Nat.instAddCommMonoid, toMul := Nat.instDistrib.toMul, left_distrib := ⋯, right_distrib := ⋯, zero_mul := ⋯, mul_zero := ⋯ }

@[implicit_reducible]

instance Nat.instNonUnitalSemiring : NonUnitalSemiring ℕ

Equations

• Nat.instNonUnitalSemiring = { toNonUnitalNonAssocSemiring := Nat.instNonUnitalNonAssocSemiring, mul_assoc := Nat.instNonUnitalSemiring._proof_1 }

@[implicit_reducible]

instance Nat.instNonAssocSemiring : NonAssocSemiring ℕ

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Nat.instSemiring : Semiring ℕ

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Nat.instCommSemiring : CommSemiring ℕ

Equations

• Nat.instCommSemiring = { toSemiring := Nat.instSemiring, mul_comm := ⋯ }

instance Nat.instCharZero : CharZero ℕ

instance Nat.instIsDomain : IsDomain ℕ