The natural numbers form a cancellative CommMonoidWithZero

This file contains the CommMonoidWithZero and IsCancelMulZero instances on the natural numbers.

See note [foundational algebra order theory].

instance Nat.instMulZeroClass : MulZeroClass ℕ

Equations

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

instance Nat.instSemigroupWithZero : SemigroupWithZero ℕ

Equations

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

instance Nat.instMonoidWithZero : MonoidWithZero ℕ

Equations

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

instance Nat.instCommMonoidWithZero : CommMonoidWithZero ℕ

Equations

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

instance Nat.instIsCancelMulZero : IsCancelMulZero ℕ

instance Nat.instMulDivCancelClass : MulDivCancelClass ℕ

instance Nat.instMulZeroOneClass : MulZeroOneClass ℕ

Equations

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