leanprover-community/mathlib

Pull Requests Commits

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

feat(algebra,equiv,logic): add various lemmas (#1342)

fpvandoorn committed 7 years ago

0dbe3a94

feat(linear_algebra/bilinear_form, linear_algebra/sesquilinear_form, ring_theory/maps): bilinear/sesquilinear forms (#1300)

amswerdlow committed 7 years ago

14024a3e

feat(data/vector2): nth_map (#1349)

ChrisHughes24 committed 7 years ago

6f747ec2

doc(tactic/ring2): document parts of ring2 (#1208)

Vtec234 committed 7 years ago

87714320

chore(data/matrix): simp attribute for transpose_tranpose (#1350)

ChrisHughes24 committed 7 years ago

Verified f3eb8c21

fix(category_theory/eq_to_hom): remove bad simp lemmas (#1346)

kim-em committed 7 years ago

5a309a3a

refactor(data/list/min_max): use with_top for maximum and define argmax (#1320)

ChrisHughes24 committed 7 years ago

9eefd40e

Newer Older