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

instance Nat.instMulOneClass : MulOneClass ℕ

Equations

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

instance Nat.instAddCancelCommMonoid : AddCancelCommMonoid ℕ

Equations

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

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.

instance Nat.instAddCommMonoid : AddCommMonoid ℕ

Equations

• Nat.instAddCommMonoid = inferInstance

instance Nat.instAddMonoid : AddMonoid ℕ

Equations

• Nat.instAddMonoid = inferInstance

instance Nat.instMonoid : Monoid ℕ

Equations

• Nat.instMonoid = inferInstance

instance Nat.instCommSemigroup : CommSemigroup ℕ

Equations

• Nat.instCommSemigroup = inferInstance

instance Nat.instSemigroup : Semigroup ℕ

Equations

• Nat.instSemigroup = inferInstance

instance Nat.instAddCommSemigroup : AddCommSemigroup ℕ

Equations

• Nat.instAddCommSemigroup = inferInstance

instance Nat.instAddSemigroup : AddSemigroup ℕ

Equations

• Nat.instAddSemigroup = inferInstance

instance Nat.instOne : One ℕ

Equations

• Nat.instOne = inferInstance

Miscellaneous lemmas

@[simp]

theorem Nat.nsmul_eq_mul (m n : ℕ) : m • n = m * n