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
instance Nat.instMulOneClass :
MulOneClass ℕ
Equations
    source
    instance Nat.instAddCancelCommMonoid :
    AddCancelCommMonoid ℕ
    Equations
      source
      instance Nat.instCommMonoid :
      CommMonoid ℕ
      Equations

        Extra instances to short-circuit type class resolution #

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

        source
        instance Nat.instAddCommMonoid :
        AddCommMonoid ℕ
        Equations
          source
          instance Nat.instAddMonoid :
          AddMonoid ℕ
          Equations
            source
            instance Nat.instMonoid :
            Monoid ℕ
            Equations
              source
              instance Nat.instCommSemigroup :
              CommSemigroup ℕ
              Equations
                source
                instance Nat.instSemigroup :
                Semigroup ℕ
                Equations
                  source
                  instance Nat.instAddCommSemigroup :
                  AddCommSemigroup ℕ
                  Equations
                    source
                    instance Nat.instAddSemigroup :
                    AddSemigroup ℕ
                    Equations
                      source
                      instance Nat.instOne :
                      One ℕ
                      Equations

                        Miscellaneous lemmas #

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