The natural numbers form a CancelCommMonoidWithZero
#
This file contains the CancelCommMonoidWithZero
instance on the natural numbers.
See note [foundational algebra order theory].
Equations
- Nat.instMulZeroClass = { toMul := instMulNat, toZero := Nat.instAddMonoid.toAddZeroClass.toZero, zero_mul := Nat.zero_mul, mul_zero := Nat.mul_zero }
Equations
- Nat.instSemigroupWithZero = { toSemigroup := Nat.instSemigroup, toZero := Nat.instMulZeroClass.toZero, zero_mul := ⋯, mul_zero := ⋯ }
Equations
- Nat.instMonoidWithZero = { toMonoid := Nat.instMonoid, toZero := Nat.instMulZeroClass.toZero, zero_mul := ⋯, mul_zero := ⋯ }
Equations
- Nat.instCommMonoidWithZero = { toCommMonoid := Nat.instCommMonoid, toZero := Nat.instMonoidWithZero.toZero, zero_mul := ⋯, mul_zero := ⋯ }
Equations
- Nat.instCancelCommMonoidWithZero = { toCommMonoidWithZero := Nat.instCommMonoidWithZero, toIsLeftCancelMulZero := Nat.instIsLeftCancelMulZero }
Equations
- One or more equations did not get rendered due to their size.