Documentation

Mathlib.Data.Nat.Basic

Algebraic instances for the natural numbers #

This file contains algebraic instances on the natural numbers and a few lemmas about them.

Implementation note #

Std has a home-baked development of the algebraic and order theoretic theory of which, in particular, is not typeclass-mediated. This is useful to set up the algebra and finiteness libraries in mathlib (naturals show up as indices in lists, cardinality in finsets, powers in groups, ...). This home-baked development is pursued in Data.Nat.Defs.

Less basic uses of should however use the typeclass-mediated development. This file is the one giving access to the algebraic instances. Data.Nat.Order.Basic is the one giving access to the algebraic order instances.

TODO #

The names of this file, Data.Nat.Defs and Data.Nat.Order.Basic are archaic and don't match up with reality anymore. Rename them.

Instances #

Extra instances to short-circuit type class resolution and ensure computability

Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations

Extra 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