The natural numbers form a CancelCommMonoidWithZero

This file contains the CancelCommMonoidWithZero instance on the natural numbers.

See note [foundational algebra order theory].

instance Nat.instMulZeroClass : MulZeroClass ℕ

Equations

• Nat.instMulZeroClass = { toMul := instMulNat, toZero := AddZeroClass.toZero, zero_mul := Nat.zero_mul, mul_zero := Nat.mul_zero }

instance Nat.instSemigroupWithZero : SemigroupWithZero ℕ

Equations

• Nat.instSemigroupWithZero = { toSemigroup := Nat.instSemigroup, toZero := MulZeroClass.toZero, zero_mul := ⋯, mul_zero := ⋯ }

instance Nat.instMonoidWithZero : MonoidWithZero ℕ

Equations

• Nat.instMonoidWithZero = { toMonoid := Nat.instMonoid, toZero := MulZeroClass.toZero, zero_mul := ⋯, mul_zero := ⋯ }

instance Nat.instCommMonoidWithZero : CommMonoidWithZero ℕ

Equations

• Nat.instCommMonoidWithZero = { toCommMonoid := Nat.instCommMonoid, toZero := MonoidWithZero.toZero, zero_mul := ⋯, mul_zero := ⋯ }

instance Nat.instIsLeftCancelMulZero : IsLeftCancelMulZero ℕ

instance Nat.instCancelCommMonoidWithZero : CancelCommMonoidWithZero ℕ

Equations

• Nat.instCancelCommMonoidWithZero = { toCommMonoidWithZero := Nat.instCommMonoidWithZero, toIsLeftCancelMulZero := Nat.instIsLeftCancelMulZero }

instance Nat.instMulDivCancelClass : MulDivCancelClass ℕ

instance Nat.instMulZeroOneClass : MulZeroOneClass ℕ

Equations

• Nat.instMulZeroOneClass = { toOne := MulOneClass.toOne, toMul := MulZeroClass.toMul, one_mul := ⋯, mul_one := ⋯, toZero := MulZeroClass.toZero, zero_mul := ⋯, mul_zero := ⋯ }