michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/algebra/algebra): add link to complete lattices module

Browse source
This commit is contained in:
Leonardo de Moura 2015-09-04 13:04:36 -07:00
parent f8a773be11
commit 3c1d6ec67a
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
library/algebra/algebra.md
View file

@ -3,11 +3,12 @@ algebra
Algebraic structures.
* [prio](prio.lean) : priority for algebraic operations
* [priority](priority.lean) : priority for algebraic operations
* [relation](relation.lean)
* [binary](binary.lean) : binary operations
* [order](order.lean)
* [lattice](lattice.lean)
* [complete lattice](complete_lattice.lean)
* [group](group.lean)
* [group_power](group_power.lean) : nat and int powers
* [group_bigops](group_bigops.lean) : products and sums over finsets
@ -18,7 +19,6 @@ Algebraic structures.
* [ring_power](ring_power.lean) : power in ring structures
* [field](field.lean)
* [ordered_field](ordered_field.lean)
* [category](category/category.md) : category theory
We set a low priority for algebraic operations, so that the elaborator tries concrete structures first.