Documentation

Mathlib.Data.Nat.Order.Basic

Algebraic order instances for the natural numbers #

This file contains algebraic order 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. Data.Nat.Basic gives access to the algebraic instances. The current file is the one giving access to the algebraic order instances.

TODO #

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

instances #

Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.

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

Equations
Equations
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
theorem NeZero.one_le {n : } [NeZero n] :
1 n