lean2/hott/algebra
Floris van Doorn 88a62f8e74 feat(algebra|types): small additions
add to markdown file for algebra, and add some definitions in types/
2015-11-22 14:21:25 -08:00
..
category feat(library/simplifier/simp_rule_set): add priorities for simp and congr rules 2015-11-16 22:34:06 -08:00
algebra.md feat(algebra|types): small additions 2015-11-22 14:21:25 -08:00
binary.hlean fix(hott): notation spacing and markdown files 2015-10-02 16:26:10 -07:00
e_closure.hlean feat(algebra/e_closure): add some support for dependent elimination of two_quotients 2015-11-16 21:32:09 -08:00
field.hlean refactor(library,hott): remove coercions between algebraic structures 2015-11-11 11:57:44 -08:00
group.hlean refactor(library,hott): remove coercions between algebraic structures 2015-11-11 11:57:44 -08:00
homotopy_group.hlean feat(homotopy/circle): give all higher homotopy groups of the circle 2015-11-22 14:21:25 -08:00
hott.hlean feat(homotopy/circle): give all higher homotopy groups of the circle 2015-11-22 14:21:25 -08:00
order.hlean refactor(library,hott): remove coercions between algebraic structures 2015-11-11 11:57:44 -08:00
ordered_group.hlean refactor(library,hott): remove coercions between algebraic structures 2015-11-11 11:57:44 -08:00
ordered_ring.hlean refactor(library,hott): remove coercions between algebraic structures 2015-11-11 11:57:44 -08:00
relation.hlean feat(hott/relation): add equivalence closure of a relation 2015-06-25 22:31:41 -04:00
ring.hlean refactor(library,hott): remove coercions between algebraic structures 2015-11-11 11:57:44 -08:00
trunc_group.hlean feat(hit): add elimination rule to propositions 2015-11-22 14:21:25 -08:00