2014-09-16 18:58:54 +00:00
|
|
|
algebra
|
|
|
|
|
=======
|
2014-08-01 17:37:55 +00:00
|
|
|
|
2014-09-16 18:58:54 +00:00
|
|
|
Algebraic structures.
|
2014-08-01 17:37:55 +00:00
|
|
|
|
2015-09-04 20:04:36 +00:00
|
|
|
* [priority](priority.lean) : priority for algebraic operations
|
2014-08-05 00:07:59 +00:00
|
|
|
* [relation](relation.lean)
|
2014-08-01 17:37:55 +00:00
|
|
|
* [binary](binary.lean) : binary operations
|
2015-08-04 02:41:37 +00:00
|
|
|
* [order](order.lean)
|
|
|
|
|
* [lattice](lattice.lean)
|
2015-09-04 20:04:36 +00:00
|
|
|
* [complete lattice](complete_lattice.lean)
|
2014-11-07 02:30:46 +00:00
|
|
|
* [group](group.lean)
|
2015-05-16 08:42:13 +00:00
|
|
|
* [group_power](group_power.lean) : nat and int powers
|
2015-12-19 19:10:20 +00:00
|
|
|
* [group_bigops](group_bigops.lean) : products and sums over lists, finsets and sets
|
2014-12-22 20:33:29 +00:00
|
|
|
* [ring](ring.lean)
|
|
|
|
|
* [ordered_group](ordered_group.lean)
|
|
|
|
|
* [ordered_ring](ordered_ring.lean)
|
2015-03-05 02:06:39 +00:00
|
|
|
* [field](field.lean)
|
2015-05-25 12:13:23 +00:00
|
|
|
* [ordered_field](ordered_field.lean)
|
2015-12-19 19:10:20 +00:00
|
|
|
* [ring_power](ring_power.lean) : power in ring structures
|
2015-12-19 20:45:24 +00:00
|
|
|
* [ring_bigops](ring_bigops.lean) : products and sums in various structures
|
2015-12-08 17:57:55 +00:00
|
|
|
* [bundled](bundled.lean) : bundled versions of the algebraic structures
|
|
|
|
|
* [category](category/category.md) : category theory (outdated, see HoTT category theory folder)
|
