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 = MulZeroClass.mk Nat.zero_mul Nat.mul_zero

instance Nat.instSemigroupWithZero : SemigroupWithZero ℕ

Equations

• Nat.instSemigroupWithZero = SemigroupWithZero.mk ⋯ ⋯

instance Nat.instMonoidWithZero : MonoidWithZero ℕ

Equations

• Nat.instMonoidWithZero = MonoidWithZero.mk ⋯ ⋯

instance Nat.instCommMonoidWithZero : CommMonoidWithZero ℕ

Equations

• Nat.instCommMonoidWithZero = CommMonoidWithZero.mk ⋯ ⋯

theorem Nat.instIsLeftCancelMulZero : IsLeftCancelMulZero ℕ

instance Nat.instCancelCommMonoidWithZero : CancelCommMonoidWithZero ℕ

Equations

• Nat.instCancelCommMonoidWithZero = CancelCommMonoidWithZero.mk

theorem Nat.instMulDivCancelClass : MulDivCancelClass ℕ

instance Nat.instMulZeroOneClass : MulZeroOneClass ℕ

Equations

• Nat.instMulZeroOneClass = MulZeroOneClass.mk ⋯ ⋯