Documentation

Mathlib.Algebra.Order.Ring.Nat

The natural numbers form an ordered semiring #

This file contains the commutative linear orderded semiring instance on the natural numbers.

See note [foundational algebra order theory].

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.
Equations
  • One or more equations did not get rendered due to their size.

Extra instances to short-circuit type class resolution #

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

Equations
Equations

Miscellaneous lemmas #

theorem Nat.isCompl_even_odd :
IsCompl {n : | Even n} {n : | Odd n}