leanprover-community/mathlib

Pull Requests Commits

mucking about with universes

kim-em committed 6 years ago

0a95a3ac

kim-em committed 6 years ago

39a69373

working, now needs lots of cleanup

kim-em committed 6 years ago

fe39160e

trying to use the simplifier rather than chain/rewrite

kim-em committed 6 years ago

69054f82

Add more complicated example

jcommelin committed 6 years ago

f2013e10

Comment out instance

jcommelin committed 6 years ago

488b2961

Merge branch 'master' into hom-tactic

jcommelin committed 6 years ago

ef7f3c5d

refactor(algebra/group): is_monoid_hom extends is_mul_hom (#915)

jcommelin committed 6 years ago

86bd577c

feat(data/set/basic): inclusion map (#906)

ChrisHughes24 committed 6 years ago

f1683a9e

refactor(category_theory): rename `functor.on_iso` to `functor.map_iso` (#893)

kim-em committed 6 years ago

96d748eb

reorganising category_theory/instances/rings.lean (#909)

kim-em committed 6 years ago

d692499e

jcommelin committed 6 years ago

2e9cfb97

Merge branch 'master' into hom-tactic

jcommelin committed 6 years ago

7ec6de1b

Add extra homs and map-lemmas

jcommelin committed 6 years ago

09d3d0c1

Clean up; add TODO

jcommelin committed 6 years ago

f6a922eb

feat(field_theory/subfield): subfields are fields (#888)

ChrisHughes24 committed 6 years ago

4494001d

chore(build): allow PRs from separate repos to test deployment scripts

cipher1024 committed 6 years ago

5c4f5f20

Make things more abstract and clunky

jcommelin committed 6 years ago

8ad4c10b

fix(mergify): require travis "push" check to push (#913)

ChrisHughes24 committed 6 years ago

c2d79f85

Add support for map_pow

jcommelin committed 6 years ago

5eb4ca4f

refactor(*): rename is_group_hom.mul to map_mul (#911)

jcommelin committed 6 years ago

66a86ffe

prototype hom tactic, with Johan

kim-em committed 6 years ago

a3d2304c

feat(order/lexicographic): lexicographic pre/partial/linear orders (#820)

kim-em committed 6 years ago

eb024dc8

feat(group_theory/subgroup): subtype.add_comm_group (#903)

ChrisHughes24 committed 6 years ago

Verified 29507a4b

feat(category_theory/colimits): missing simp lemmas (#894)

kim-em committed 6 years ago

ec51b6e1

fix(doc/extra/tactic_writing): rename mul_left (#902) [ci skip]

minchaowu committed 6 years ago

6d2cf4ae

feat(linear_algebra/dual): add dual vector spaces (#881)

faabian committed 6 years ago

5f1329a2

feat(analysis/complex/polynomial): fundamental theorem of algebra (#851)

ChrisHughes24 committed 6 years ago

10490ea7

feat(topology/gromov_hausdorff): the Gromov-Hausdorff space (#883)

sgouezel committed 6 years ago

4fecb101

trying to work out what was wrong with catching signals (#898)

kim-em committed 6 years ago

5d81ab17

Older