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 = MulOneClass.mk Nat.one_mul Nat.mul_one

instance Nat.instAddCancelCommMonoid : AddCancelCommMonoid ℕ

Equations

• Nat.instAddCancelCommMonoid = AddCancelCommMonoid.mk ⋯

instance Nat.instCommMonoid : CommMonoid ℕ

Equations

• Nat.instCommMonoid = CommMonoid.mk Nat.mul_comm

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

Miscellaneous lemmas

@[simp]

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