leanprover-community/mathlib

Pull Requests Commits

fix(category_theory): turn `has_limits` classes into structures (#896)

kim-em committed 6 years ago

0a490302

feat(data/list/min_max): add minimum (#892)

minchaowu committed 6 years ago

483a6c23

feat(subgroup, subring, subfield): directed Unions of subrings are subrings (#889)

ChrisHughes24 committed 6 years ago

891c0506

feat(field_theory/subfield): is_subfield instances (#891)

ChrisHughes24 committed 6 years ago

Verified bd524fc1

feat(data/nat/basic): b = c if b - a = c - a (#862)

kim-em committed 6 years ago

7e70ebd0

fix(build): external PRs can't use GitHub credentials

cipher1024 committed 6 years ago

3000f328

fix(analysis/normed_space/bounded_linear_maps): fix build (#895)

ChrisHughes24 committed 6 years ago

Verified e4d3ca31

refactor(analysis/normed_space/bounded_linear_maps): nondiscrete normed field

sgouezel committed 6 years ago

31ff5c5c

fix(appveyor): build every commit

cipher1024 committed 6 years ago

53e7d724

refactor(analysis/normed_space/bounded_linear_maps): nondiscrete normed field

sgouezel committed 6 years ago

ae8a1fb6

chore(mergify): require the AppVeyor build to succeed

cipher1024 committed 6 years ago

8831e0a7

fix(scripts): not all files were deployed through the curl command (#879)

cipher1024 committed 6 years ago

Verified 8fa071f4

feat(category_theory/bifunctor): simp lemmas (#867)

kim-em committed 6 years ago

8d45ccb7

more general hypotheses for integer induction (#885)

abhimanyupallavisudhir committed 6 years ago

3360f98a

feat(algebra/opposites): opposites of operators (#538)

kckennylau committed 6 years ago

d8a2bc51

fix(build): match build names

cipher1024 committed 6 years ago

e0e231da

fix(scripts): protect `leanpkg test` against timeouts

cipher1024 committed 6 years ago

d0f86077

fix(scripts): Mac Python's test support doesn't work on Travis

cipher1024 committed 6 years ago

e809df6d

fix(scripts): not all files were deployed through the curl command

cipher1024 committed 6 years ago

d9ec8a82

feat(data/mllist): monadic lazy lists (#865)

kim-em committed 6 years ago

78a08ebc

feat(list.split_on): [1,1,2,3,2,4,4].split_on 2 = [[1,1],[3],[4,4]] (#866)

kim-em committed 6 years ago

44d1c7aa

feat(data/list/min_max): minimum and maximum over list (#884)

minchaowu committed 6 years ago

901bdbf4

feat(data/matrix): more basic matrix lemmas (#873)

abentkamp committed 6 years ago

858d111c

feat(category_theory): introduce the core of a category (#832)

kim-em committed 6 years ago

0b7ee1b4

chore(mergify): delete head branch when merging

cipher1024 committed 6 years ago

b6c2be42

feat(algebra/char_p,field_theory/finite_card): cardinality of finite fields (#819)

CPutz committed 6 years ago

7aaccae7

chore(github/pr): enable code owners

cipher1024 committed 6 years ago

3abfda0e

feat(data/list/perm): nil_subperm (#882)

minchaowu committed 6 years ago

8183a5a6

feat (analysis/normed_space/basic.lean): implement reverse triangle inequality (#831)

jdsalchow committed 6 years ago

384c9be2

fix(build): fix Lean version

cipher1024 committed 6 years ago

07aa1e3e

Newer Older