leanprover-community/mathlib3

Pull Requests Commits

kim-em committed 7 years ago

adb03f6f

feat(category_theory/option): instances

kim-em committed 7 years ago

fdcaf230

chore(unicode): improve arrows (#1373)

khoek committed 7 years ago

455f0603

doc(contribute): add detailed instructions for cache-olean [skip ci] (#1367)

fpvandoorn committed 7 years ago

4c5c4dc7

feat(sanity_check): improve sanity_check (#1369)

fpvandoorn committed 7 years ago

2db7fa45

feat(category_theory/limits): special shapes (#1339)

kim-em committed 7 years ago

afe51c76

Fix `tactic.exact` timeout in `apply'` (#1371)

Zhouhang Zhou committed 7 years ago

1278efd6

feat(analysis/calculus/times_cont_diff): adding a lemma (#1358)

sgouezel committed 7 years ago

1ff35858

refactor(category_theory/single_obj): migrate to bundled morphisms (#1330)

urkud committed 7 years ago

3b195032

fix(tactic.basic): add sanity_check import (#1365)

fpvandoorn committed 7 years ago

d4c1c0f6

fix(topology/uniform_space): sanity_check pass (#1364)

PatrickMassot committed 7 years ago

721d67a7

refactor: change field notation from k to \bbk (#1363)

sgouezel committed 7 years ago

79dccba9

fix(topology/algebra/uniform_group): tiny priority tweak

PatrickMassot committed 7 years ago

45df75b3

chore(algebra/ring): change semiring_hom to ring_hom (#1361)

101damnations committed 7 years ago

cc04ba7e

feat(data/rat): add lt, le, and eq def lemmas, move casts into rat to basic (#1348)

kappelmann committed 7 years ago

914c572e

feat(data/fin): coe_eq_val and coe_mk (#1321)

ChrisHughes24 committed 7 years ago

7bc18a84

fix(docs/install): resize extensions icons for consistency [ci skip]

Patrick Massot committed 7 years ago

253a9f7d

doc(install/*): new VS-code icon [ci skip]

Patrick Massot committed 7 years ago

91a9b4bb

feat(tactic/apply'): apply without unfolding type definitions (#1234)

cipher1024 committed 7 years ago

9a425726

fix(tactic/tauto): use intro1 to deal with negations (#1354)

robertylewis committed 7 years ago

f74cc70c

feat(*): small lemmas from the sensitivity formalization (#1352)

robertylewis committed 7 years ago

40b09aab

docs(category/monad,bitraversable): add module docstrings #1260 (#1286)

cipher1024 committed 7 years ago

f442a41a

Rename Groupoid.lean to groupoid_category.lean (#1353)

ChrisHughes24 committed 7 years ago

Verified a489719b

feat(category_theory/Groupoid): category of groupoids (#1325)

urkud committed 7 years ago

8de4273b

feat(conv/conv): conv tactics for zooming/saving state (#1351)

khoek committed 7 years ago

35144f27

feat(archive): add the cubing a cube proof (#1343)

fpvandoorn committed 7 years ago

3f915fc5

refactor(*): rewrite `to_additive` attribute (#1345)

urkud committed 7 years ago

c5128756

chore(gitignore): ignore files generated by mk_all script (#1328)

robertylewis committed 7 years ago

733f616f

feat(tactic/lift): add lift tactic (#1315)

fpvandoorn committed 7 years ago

80700498

chore(category_theory/monoidal): monoidal_category doesn't extend category (#1338)

kim-em committed 7 years ago

26a3e31d

Older