Mathlib.Algebra.Group.Nat.Defs

Module docstring

{"# 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 ","### Extra instances to short-circuit type class resolution

These also prevent non-computable instances being used to construct these instances non-computably. ","### Miscellaneous lemmas "}

Nat.instMulOneClass instance

: MulOneClass ℕ

Full source

instance instMulOneClass : MulOneClass ℕ where
  one_mul := Nat.one_mul
  mul_one := Nat.mul_one

Natural Numbers as a Multiplicative Monoid

Informal description

The natural numbers $\mathbb{N}$ form a multiplicative monoid with identity element $1$.

Nat.instAddCancelCommMonoid instance

: AddCancelCommMonoid ℕ

Full source

instance instAddCancelCommMonoid : AddCancelCommMonoid ℕ where
  add := Nat.add
  add_assoc := Nat.add_assoc
  zero := Nat.zero
  zero_add := Nat.zero_add
  add_zero := Nat.add_zero
  add_comm := Nat.add_comm
  nsmul m n := m * n
  nsmul_zero := Nat.zero_mul
  nsmul_succ := succ_mul
  add_left_cancel _ _ _ := Nat.add_left_cancel

Natural Numbers as an Additive Cancellative Commutative Monoid

Informal description

The natural numbers $\mathbb{N}$ form an additive cancellative commutative monoid.

Nat.instCommMonoid instance

: CommMonoid ℕ

Full source

instance instCommMonoid : CommMonoid ℕ where
  mul := Nat.mul
  mul_assoc := Nat.mul_assoc
  one := Nat.succ Nat.zero
  one_mul := Nat.one_mul
  mul_one := Nat.mul_one
  mul_comm := Nat.mul_comm
  npow m n := n ^ m
  npow_zero := Nat.pow_zero
  npow_succ _ _ := rfl

Natural Numbers as a Commutative Monoid

Informal description

The natural numbers $\mathbb{N}$ form a commutative monoid under multiplication.

Nat.instAddCommMonoid instance

: AddCommMonoid ℕ

Full source

instance instAddCommMonoid    : AddCommMonoid ℕ    := by infer_instance

Natural Numbers as an Additive Commutative Monoid

Informal description

The natural numbers $\mathbb{N}$ form an additive commutative monoid.

Nat.instAddMonoid instance

: AddMonoid ℕ

Full source

instance instAddMonoid        : AddMonoid ℕ        := by infer_instance

Natural Numbers as an Additive Monoid

Informal description

The natural numbers $\mathbb{N}$ form an additive monoid.

Nat.instMonoid instance

: Monoid ℕ

Full source

instance instMonoid           : Monoid ℕ           := by infer_instance

Natural Numbers as a Monoid

Informal description

The natural numbers $\mathbb{N}$ form a monoid under multiplication.

Nat.instCommSemigroup instance

: CommSemigroup ℕ

Full source

instance instCommSemigroup    : CommSemigroup ℕ    := by infer_instance

Natural Numbers as a Commutative Semigroup

Informal description

The natural numbers $\mathbb{N}$ form a commutative semigroup under addition.

Nat.instSemigroup instance

: Semigroup ℕ

Full source

instance instSemigroup        : Semigroup ℕ        := by infer_instance

Natural Numbers as an Additive Semigroup

Informal description

The natural numbers $\mathbb{N}$ form a semigroup under addition.

Nat.instAddCommSemigroup instance

: AddCommSemigroup ℕ

Full source

instance instAddCommSemigroup : AddCommSemigroup ℕ := by infer_instance

Natural Numbers as an Additive Commutative Semigroup

Informal description

The natural numbers $\mathbb{N}$ form an additive commutative semigroup.

Nat.instAddSemigroup instance

: AddSemigroup ℕ

Full source

instance instAddSemigroup     : AddSemigroup ℕ     := by infer_instance

Natural Numbers as an Additive Semigroup

Informal description

The natural numbers $\mathbb{N}$ form an additive semigroup under addition.

Nat.instOne instance

: One ℕ

Full source

instance instOne : One ℕ := inferInstance

The Multiplicative Identity on Natural Numbers

Informal description

The natural numbers $\mathbb{N}$ have a distinguished element $1$ that serves as the multiplicative identity.

Nat.nsmul_eq_mul theorem

(m n : ℕ) : m • n = m * n

Full source

@[simp 900] protected lemma nsmul_eq_mul (m n : ℕ) : m • n = m * n := rfl

Scalar Multiplication Equals Multiplication in Natural Numbers

Informal description

For any natural numbers $m$ and $n$, the scalar multiplication $m \cdot n$ is equal to the product $m \times n$.