leanprover-community/mathlib3

Pull Requests Commits

feat(option/injective_map) (#978)

kim-em committed 6 years ago

Verified c7baf8ef

feat(tactic/decl_mk_const): performance improvement for library_search (#967)

kim-em committed 6 years ago

f98ffdef

chore(build): build only master and its related PRs

cipher1024 committed 6 years ago

7b1105bf

chore(README): put the badges in the README on one line (#975)

jcommelin committed 6 years ago

e747c91c

feat(docs/install_debian): Debian startup guide (#974)

PatrickMassot committed 6 years ago

f2db6369

feat(category_theory/limits): support for special shapes of (co)limits (#938)

kim-em committed 6 years ago

Verified f5060c40

chore(travis): disable the check for minimal imports (#973)

jcommelin committed 6 years ago

Verified 219cb1a1

chore(docs): delete docs/wip.md (#972)

kim-em committed 6 years ago

44386cde

remove code duplication (#971)

kim-em committed 6 years ago

3eb7ebca

fix(data/polynomial): change instance order in polynomial.subsingleton (#970)

robertylewis committed 6 years ago

6956daa2

fix(scripts/remote-install-update-mathlib): apt shouldn't ask (#969)

PatrickMassot committed 6 years ago

60b3c198

fix(script/remote-install-update-mathlib) fix answer reading and requests/urllib3 version conflict (#968)

PatrickMassot committed 6 years ago

d2889058

feat(ring_theory/ideal_operations): inj_iff_trivial_ker for ring homomorphisms (#951)

ramonfmir committed 6 years ago

8a097f13

feat(category_theory/limits/opposites): (co)limits in opposite categories (#926)

kim-em committed 6 years ago

ef11fb3d

fix(tactic/library_search): iff lemmas with universes (#935)

kim-em committed 6 years ago

69094fcf

feat(category_theory/limits): complete lattices have (co)limits (#931)

kim-em committed 6 years ago

9b7fb5fd

feat(script/auth_github): improve messages [ci skip] (#965)

PatrickMassot committed 6 years ago

b3433a51

chore(category_theory): move small_category_of_preorder to preorder namespace (#932)

kim-em committed 6 years ago

c8a2aa95

fix(scripts/remote-install-update-mathlib): try again [ci skip]

Patrick Massot committed 6 years ago

7c868148

fix(scripts/remote-install-update-mathlib): missing dependency (#964)

PatrickMassot committed 6 years ago

a15fca5d

feat(analysis/normed_space): open mapping (#900)

sgouezel committed 6 years ago

8dcce05f

refactor(tactic/interactive): remove dependencies of (#878)

cipher1024 committed 6 years ago

00aaf05a

jcommelin committed 6 years ago

Verified 9b3e91b0

refactor(analysis/normed_space): use bundled type for `fderiv` (#956)

jlpaca committed 6 years ago

53f98786

fix(README): update maintainer list

PatrickMassot committed 6 years ago

Verified b49bf61c

feat(data/equiv/basic): sum_compl_apply and others (#961)

ChrisHughes24 committed 6 years ago

Verified 0444f9c2

refactor(analysis/normed_space/operator_norm): replace subspace with … (#955)

sgouezel committed 6 years ago

038f809c

feat(function/embedding): ext and ext_iff (#962)

ChrisHughes24 committed 6 years ago

1d9ff681

fix(ring_theory/adjoin_root): move adjoin_root out of adjoin_root namespace (#960)

ChrisHughes24 committed 6 years ago

0d7b4195

refactor(data/equiv/basic): simplify definition of equiv.set.range (#959)

ChrisHughes24 committed 6 years ago

45456cf1

Newer Older