lean2/library/algebra/algebra.md

algebra
=======

Algebraic structures.

* [priority](priority.lean) : priority for algebraic operations
* [relation](relation.lean)
* [binary](binary.lean) : binary operations
* [order](order.lean)
* [interval](interval.lean)
* [lattice](lattice.lean)
* [complete lattice](complete_lattice.lean)
* [galois_connection](galois_connection.lean)
* [group](group.lean)
* [group_power](group_power.lean) : nat and int powers
* [group_bigops](group_bigops.lean) : products and sums over lists, finsets and sets
* [ring](ring.lean)
* [ordered_group](ordered_group.lean)
* [ordered_ring](ordered_ring.lean)
* [field](field.lean)
* [ordered_field](ordered_field.lean)
* [module](module.lean) : modules, vector spaces, and linear maps
* [ring_power](ring_power.lean) : power in ring structures
* [ring_bigops](ring_bigops.lean) : products and sums in various structures
* [order_bigops](order_bigops.lean) : min and max over finsets and finite sets
* [bundled](bundled.lean) : bundled versions of the algebraic structures
* [monotone](monotone.lean) : monotone maps between order structures
* [homomorphism](homomorphism.lean) : homomorphisms between algebraic structures
* [category](category/category.md) : category theory (outdated, see HoTT category theory folder)
refactor(library): rename algebra directory to struc, move categories.lean to algebra 2014-09-16 18:58:54 +00:00			`algebra`
			`=======`
feat(library/standard): add markdown documentation 2014-08-01 17:37:55 +00:00
refactor(library): rename algebra directory to struc, move categories.lean to algebra 2014-09-16 18:58:54 +00:00			`Algebraic structures.`
feat(library/standard): add markdown documentation 2014-08-01 17:37:55 +00:00
feat(library/algebra/algebra): add link to complete lattices module 2015-09-04 20:04:36 +00:00			`* [priority](priority.lean) : priority for algebraic operations`
feat(library/standard): add classes for relations 2014-08-05 00:07:59 +00:00			`* [relation](relation.lean)`
feat(library/standard): add markdown documentation 2014-08-01 17:37:55 +00:00			`* [binary](binary.lean) : binary operations`
refactor(library/algebra/{lattice,order},library/data/nat): split lattice from order, make nat an instance of discrete linear order 2015-08-04 02:41:37 +00:00			`* [order](order.lean)`
feat(library/data/nat/bigops): sums and products over intervals of natural numbers 2015-12-31 20:51:20 +00:00			`* [interval](interval.lean)`
refactor(library/algebra/{lattice,order},library/data/nat): split lattice from order, make nat an instance of discrete linear order 2015-08-04 02:41:37 +00:00			`* [lattice](lattice.lean)`
feat(library/algebra/algebra): add link to complete lattices module 2015-09-04 20:04:36 +00:00			`* [complete lattice](complete_lattice.lean)`
feat(library/algebra): add theory about Galois connections Adds a small theory about Galois connections, i.e. order theoretic adjoints, and their relations to least upper and greatest lower bounds. 2016-01-04 21:15:02 +00:00			`* [galois_connection](galois_connection.lean)`
feat(library/algebra/group): add multiplicative and additive structures 2014-11-07 02:30:46 +00:00			`* [group](group.lean)`
refactor,feat(library/{data,algebra}): move bigops to algebra, define sums 2015-05-16 08:42:13 +00:00			`* [group_power](group_power.lean) : nat and int powers`
refactor(library/algebra): combine group_bigops and group_set_bigops 2015-12-19 19:10:20 +00:00			`* [group_bigops](group_bigops.lean) : products and sums over lists, finsets and sets`
refactor(library): clean up headers and markdown files 2014-12-22 20:33:29 +00:00			`* [ring](ring.lean)`
			`* [ordered_group](ordered_group.lean)`
			`* [ordered_ring](ordered_ring.lean)`
feat(*.md): create markdown files for HoTT library, update ones in standard library 2015-03-05 02:06:39 +00:00			`* [field](field.lean)`
refactor(library/*): do various renamings 2015-05-25 12:13:23 +00:00			`* [ordered_field](ordered_field.lean)`
feat(library/algebra/module): make a start on modules and vector spaces (with material from Nathaniel Thomas) 2015-12-22 17:54:42 +00:00			`* [module](module.lean) : modules, vector spaces, and linear maps`
refactor(library/algebra): combine group_bigops and group_set_bigops 2015-12-19 19:10:20 +00:00			`* [ring_power](ring_power.lean) : power in ring structures`
feat(library/algebra/ring_bigops): make start on file with more properties of sums and products 2015-12-19 20:45:24 +00:00			`* [ring_bigops](ring_bigops.lean) : products and sums in various structures`
feat(library/algebra/order_bigops): add min and max over finsets and finite sets 2016-01-24 21:46:31 +00:00			`* [order_bigops](order_bigops.lean) : min and max over finsets and finite sets`
feat(hott/algebra): port abstract structures 2015-12-08 17:57:55 +00:00			`* [bundled](bundled.lean) : bundled versions of the algebraic structures`
feat(library/algebra/monotone): add properties of monotone functions 2016-02-29 02:55:48 +00:00			`* [monotone](monotone.lean) : monotone maps between order structures`
feat(library/algebra/homomorphism): add homomorphisms between algebraic structures 2016-02-28 14:39:43 +00:00			`* [homomorphism](homomorphism.lean) : homomorphisms between algebraic structures`
feat(hott/algebra): port abstract structures 2015-12-08 17:57:55 +00:00			`* [category](category/category.md) : category theory (outdated, see HoTT category theory folder)`