leanprover-community/mathlib

Pull Requests Commits

kim-em committed 5 years ago

d87e8ac4

lets make life easy

kim-em committed 5 years ago

a6d7736f

kim-em committed 5 years ago

1a074f07

docs(install/*): put extra emphasis (#2439)

jcommelin committed 5 years ago

1ef989f8

feat(tactic/lint): lint for missing has_coe_to_fun instances (#2437)

gebner committed 5 years ago

6b095759

fix(github/workflows): ignore new bors branch (#2441)

gebner committed 5 years ago

24d464c6

chore(scripts): update nolints.txt (#2440)

leanprover-community-bot committed 5 years ago

da292759

chore(*): migrate `nat/int/rat.eq_cast` to bundled homs (#2427)

urkud committed 5 years ago

64f6903e

feat(data/nat): Results about nat.choose (#2421)

b-mehta committed 5 years ago

855e70bf

feat(analysis/analytic/composition): the composition of analytic functions is analytic (#2399)

sgouezel committed 5 years ago

0bc15f82

chore(scripts): update nolints.txt (#2436)

leanprover-community-bot committed 5 years ago

715be9f7

feat(category_theory/limits): strong epimorphisms and strong epi-mono factorizations (#2433)

TwoFX committed 5 years ago

0567b7fa

feat(category_theory): creation of limits and reflection of isomorphisms (#2426)

b-mehta committed 5 years ago

f3471479

chore(scripts): update nolints.txt (#2435)

leanprover-community-bot committed 5 years ago

0d3e5465

chore(algebra/lie_algebra): add function coercion for morphisms (#2434)

Oliver Nash committed 5 years ago

d2db3e83

feat(computability): strong reducibility and degrees (#1203)

minchaowu committed 5 years ago

c3d943e2

chore(scripts): update nolints.txt (#2432)

leanprover-community-bot committed 5 years ago

a113d6e6

feat(analysis/calculus): let simp compute derivatives (#2422)

sgouezel committed 5 years ago

846cbabb

refactor(analysis/asymptotics): make is_o irreducible (#2416)

sgouezel committed 5 years ago

ec800611

refactor(tactic/norm_cast): simplified attributes and numeral support (#2407)

gebner committed 5 years ago

5fd4afc4

chore(scripts): update nolints.txt (#2430)

leanprover-community-bot committed 5 years ago

7270af9c

feat(category_theory): connected categories (#2413)

b-mehta committed 5 years ago

5ac2b48c

feat(data/finset): existence of a smaller set (#2420)

b-mehta committed 5 years ago

66cc2980

chore(scripts): update nolints.txt (#2425)

leanprover-community-bot committed 5 years ago

8510f07e

fix(data/zmod/basic): typo (#2424)

kbuzzard committed 5 years ago

1e212d7d

feat(category_theory/limits): special shapes API cleanup (#2423)

TwoFX committed 5 years ago

ce72cde8

feat(library_search): (efficiently) try calling symmetry before searching the library (#2415)

kim-em committed 5 years ago

9b797ee3

chore(category_theory/limits): remove dependency on concrete_categories (#2411)

kim-em committed 5 years ago

8e8037f5

chore(scripts): update nolints.txt (#2418)

leanprover-community-bot committed 5 years ago

fd0dc27e

refactor(analysis/calculus/deriv): split comp and scomp (#2410)

sgouezel committed 5 years ago

96a07a71

Older