leanprover-community/mathlib3

Pull Requests Commits

chore(algebra/module): replace typeclass arguments with inferred arguments (#2444)

kim-em committed 5 years ago

11d89a2f

feat(data/nat/prime) factors of a prime number is the list [p] (#2452)

alexjbest committed 5 years ago

0ceac44d

chore(*): switch to lean 3.9.0 (#2449)

gebner committed 5 years ago

99245b33

feat(category_theory/limits/over): over category has connected limits (#2438)

b-mehta committed 5 years ago

d76a882d

fix(*): remove `@[nolint simp_nf]` (#2450)

gebner committed 5 years ago

8ec447d8

fix(docs/extra/calc.md): remove extra space (#2448)

bryangingechen committed 5 years ago

5107c2bd

fix(group_theory/submonoid): looping simp lemma (#2447)

gebner committed 5 years ago

16552e6a

feat(tactic/transport): transport structures across equivalences (#2251)

kim-em committed 5 years ago

4e872238

chore(algebra/group/type_tags): add `additive.to_mul` etc (#2363)

urkud committed 5 years ago

ffb99a33

chore(data/mv_polynomial): adding a comment about a T50000 regression (#2442)

kim-em committed 5 years ago

8b21231c

refactor(data/nat/fib): simplify proof of fib_succ_succ (#2443)

lambda-fairy committed 5 years ago

a530a817

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

Newer Older