lean2/library/data/nat/nat.md

data.nat
========

The natural numbers.

* [basic](basic.lean) : the natural numbers, with succ, pred, addition, and multiplication
* [order](order.lean) : less-than, less-then-or-equal, etc.
* [bquant](bquant.lean) : bounded quantifiers
* [sub](sub.lean) : subtraction, and distance
* [div](div.lean) : div and mod
* [gcd](gcd.lean) : gcd, lcm, and coprime
* [power](power.lean)
* [bigops](bigops.lean) : finite sums and products
* [find](find.lean) : search for a witness to an existence statement
feat(library/standard): add markdown documentation 2014-08-01 17:37:55 +00:00			`data.nat`
			`========`

			`The natural numbers.`

feat(library/standard/data/nat): port most recent nat to lean 0.2 2014-08-02 01:40:24 +00:00			`* [basic](basic.lean) : the natural numbers, with succ, pred, addition, and multiplication`
			`* [order](order.lean) : less-than, less-then-or-equal, etc.`
feat(library/data/nat): make nat an instance of comm_semiring 2014-12-24 00:46:48 +00:00			`* [bquant](bquant.lean) : bounded quantifiers`
feat(library/standard/data/nat/div): port div 2014-08-21 00:21:14 +00:00			`* [sub](sub.lean) : subtraction, and distance`
refactor(library/data/nat/gcd.lean): move gcd to a new file 2015-05-29 07:37:18 +00:00			`* [div](div.lean) : div and mod`
			`* [gcd](gcd.lean) : gcd, lcm, and coprime`
refactor,feat(library/{data,algebra}): move bigops to algebra, define sums 2015-05-16 08:42:13 +00:00			`* [power](power.lean)`
fix(library/data/nat/nat.md): add 'find' to markdown file 2015-07-27 03:26:07 +00:00			`* [bigops](bigops.lean) : finite sums and products`
			`* [find](find.lean) : search for a witness to an existence statement`