Lean mathematical components library
Switch branches/tags
Nothing to show
Clone or download
Latest commit 8c385bc Nov 18, 2018
Permalink
Failed to load latest commit information.
algebra refactor(algebra/euclidean_domain): euclidean_domain extends nonzero_… Nov 15, 2018
analysis fix(analysis/topology/topological_structures): remove useless decidab… Nov 15, 2018
category feat(category/bifunctor): Bifunctor and bitraversable (#255) Nov 5, 2018
category_theory feat(category_theory): associator and unitors for functors (#478) Nov 18, 2018
computability feat(data/nat/basic): a few choiceless proofs Oct 10, 2018
core feat(tactic/ext): address reviewers' comments Sep 11, 2018
data refactor(order/complete_lattice): define supr and infi with range (#474) Nov 14, 2018
docs feat(category_theory): propose removing coercions from category_theor… Nov 8, 2018
field_theory feat(field_theory/perfect_closure): define the perfect closure of a f… Nov 5, 2018
group_theory feat(ring_theory/ideal_operations): define ideal operations (multipli… Nov 8, 2018
linear_algebra refactor(order/complete_lattice): define supr and infi with range (#474) Nov 14, 2018
logic chore(*): clean up uses of zorn Nov 9, 2018
meta refactor(tactic/linarith): refactoring Sep 10, 2018
number_theory feat(data/zmod/quadratic_reciprocity): quadratic reciprocity (#327) Oct 1, 2018
order refactor(order/complete_lattice): define supr and infi with range (#474) Nov 14, 2018
pending feat(data/real): reals from first principles Jan 15, 2018
ring_theory fix(ring_theory/subring): unnecessary classical (#482) Nov 17, 2018
set_theory feat(linear_algebra,ring_theory): refactoring modules (#456) Nov 5, 2018
tactic fix(tactic/basic): use `lean.parser.of_tactic'` instead of builtin Nov 13, 2018
tests fix(tactic/basic): use `lean.parser.of_tactic'` instead of builtin Nov 13, 2018
.gitignore refactor(*): import content from lean/library/data and library_dev Jul 23, 2017
.travis.yml fix(travis.yml): adding a third stage to the travis build (#281) Aug 27, 2018
LICENSE Initial commit Jul 21, 2017
PULL_REQUEST_TEMPLATE.md docs(code-review): add check list (#195) [ci-skip] Jul 16, 2018
README.md doc(hole/instance_stub) (#400) Oct 7, 2018
leanpkg.toml chore(leanpkg.toml): update version to 3.4.1 May 25, 2018
travis_long.sh chore(build): make travis build fail quicker when errors are found Jul 16, 2018

README.md

mathlib

Build Status

Lean standard library

Besides Lean's general documentation, the documentation of mathlib consists of:

This repository also contains extra Lean documentation not specific to mathlib.