lean2/hott/algebra/algebra.md
Floris van Doorn 8072fdf9a0 linkfix
closes #11
2018-10-01 16:13:23 -04:00

1.7 KiB

algebra

The following files are ported from the standard library. If anything needs to be changed, it is probably a good idea to change it in the standard library and then port the file again (see also script/port.pl).

Files which are not ported from the standard library:

  • inf_group : algebraic structures which are not assumes to be sets. No higher coherences are assumed. Truncated algebraic structures extend these structures with the assumption that they are sets.
  • inf_group_theory : Some very basic group theory using InfGroups
  • group_theory : Basic theorems about group homomorphisms and isomorphisms
  • trunc_group : truncate an infinity-group to a group
  • homotopy_group : homotopy groups of a pointed type
  • e_closure : the type of words formed by a relation, or paths in a graph.
  • graph : definition and operations on paths in a graph.

Subfolders (not ported):