# The natural numbers form a monoid #

This file contains the additive and multiplicative monoid instances on the natural numbers.

See note [foundational algebra order theory].

### Instances #

source
instance Nat.instMulOneClass :
MulOneClass ℕ
Equations

- Nat.instMulOneClass = { toOne := One.ofOfNat1, toMul := instMulNat, one_mul := Nat.one_mul, mul_one := Nat.mul_one }

source
instance Nat.instAddCancelCommMonoid :
AddCancelCommMonoid ℕ
Equations

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

source
instance Nat.instCommMonoid :
CommMonoid ℕ
Equations

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

### Extra instances to short-circuit type class resolution #

These also prevent non-computable instances being used to construct these instances non-computably.

source
instance Nat.instAddCommMonoid :
AddCommMonoid ℕ
Equations

- Nat.instAddCommMonoid = inferInstance

source
instance Nat.instAddMonoid :
AddMonoid ℕ
Equations

- Nat.instAddMonoid = inferInstance

source
instance Nat.instMonoid :
Monoid ℕ
Equations

- Nat.instMonoid = inferInstance

source
instance Nat.instCommSemigroup :
CommSemigroup ℕ
Equations

- Nat.instCommSemigroup = inferInstance

source
instance Nat.instSemigroup :
Semigroup ℕ
Equations

- Nat.instSemigroup = inferInstance

source
instance Nat.instAddCommSemigroup :
AddCommSemigroup ℕ
Equations

- Nat.instAddCommSemigroup = inferInstance

source
instance Nat.instAddSemigroup :
AddSemigroup ℕ
Equations

- Nat.instAddSemigroup = inferInstance

source
instance Nat.instOne :
One ℕ
Equations

- Nat.instOne = inferInstance

source
instance Nat.instIsAddTorsionFree :
IsAddTorsionFree ℕ

### Miscellaneous lemmas #

source
@[simp]
theorem Nat.nsmul_eq_mul (m n : ℕ) :
m • n = m * n