Documentation

Mathlib.Algebra.Group.Nat.Defs

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
🔸 coverage
@[implicit_reducible]
instance Nat.instMulOneClass :
MulOneClass ℕ
source
🔸 coverage
@[implicit_reducible]
instance Nat.instAddCancelCommMonoid :
AddCancelCommMonoid ℕ
source
🔸 coverage
@[implicit_reducible]
instance Nat.instCommMonoid :
CommMonoid ℕ
source
📐 coverage
instance Nat.instIsMulTorsionFree :
IsMulTorsionFree ℕ
source
📐 coverage
instance Nat.instIsAddTorsionFree :
IsAddTorsionFree ℕ

Extra instances to short-circuit type class resolution #

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

source
🔸 coverage
@[implicit_reducible]
instance Nat.instAddCommMonoid :
AddCommMonoid ℕ
source
🔸 coverage
@[implicit_reducible]
instance Nat.instAddMonoid :
AddMonoid ℕ
source
🔸 coverage
@[implicit_reducible]
instance Nat.instMonoid :
Monoid ℕ
source
🔸 coverage
@[implicit_reducible]
instance Nat.instCommSemigroup :
CommSemigroup ℕ
source
🔸 coverage
@[implicit_reducible]
instance Nat.instSemigroup :
Semigroup ℕ
source
🔸 coverage
@[implicit_reducible]
instance Nat.instAddCommSemigroup :
AddCommSemigroup ℕ
source
🔸 coverage
@[implicit_reducible]
instance Nat.instAddSemigroup :
AddSemigroup ℕ
source
🔸 coverage
@[implicit_reducible]
instance Nat.instOne :
One ℕ

Miscellaneous lemmas #

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