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.instAddCommMonoid : AddCommMonoid ℕ

Equations

• Nat.instAddCommMonoid = AddCommMonoid.mk Nat.add_comm

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.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

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

theorem Nat.toAdd_pow (a : Multiplicative ℕ) (b : ℕ) : Multiplicative.toAdd (a ^ b) = Multiplicative.toAdd a * b

@[simp]

theorem Nat.ofAdd_mul (a : ℕ) (b : ℕ) : Multiplicative.ofAdd (a * b) = Multiplicative.ofAdd a ^ b