leanprover-community/mathlib3

Pull Requests Commits

chore(meta/expr): add a docstring (#2487)

khoek committed 5 years ago

f760ad5f

feat(data/option): add `option.mmap` and `option.maybe` (#2484)

khoek committed 5 years ago

62a613fa

chore(data/polynomial): rename type vars (#2483)

urkud committed 5 years ago

e4abcedc

feat(data/monoid_algebra): algebra structure, lift of morphisms (#2366)

urkud committed 5 years ago

59653709

chore(cmd/where): remove unused argument (#2486)

khoek committed 5 years ago

142f0017

feat(group_theory/bundled_subgroup): bundled subgroup (#2140)

kex-y committed 5 years ago

5e2025f6

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

leanprover-community-bot committed 5 years ago

585d77ae

fix(tactic/where): remove hackery from `#where`, using Lean 3c APIs (#2465)

khoek committed 5 years ago

ffa97d0f

feat(tactic/hint): if hint can solve the goal, say so (#2474)

kim-em committed 5 years ago

533a5523

feat(tactic/#simp): a user_command for #simp (#2446)

kim-em committed 5 years ago

15d35b1a

fix(tactic/clear): don't use rb_map unnecessarily (#2325)

kim-em committed 5 years ago

df84064e

fix(category_theory/concrete): access the carrier type by the coercion (#2473)

kim-em committed 5 years ago

3edb6a4a

chore(category_theory): delete two empty files (#2472)

kim-em committed 5 years ago

7a13a11a

chore(docs/naming): update (#2468)

kim-em committed 5 years ago

5d0a7240

fix(algebra/category/*/colimits): cleaning up (#2469)

kim-em committed 5 years ago

76267637

feat(data/nat,data/int): add some modular arithmetic lemmas (#2460)

jsm28 committed 5 years ago

8adfafd9

feat(category_theory/faithful): faithful.of_iso (#2453)

kim-em committed 5 years ago

d1ba87a9

feat(data/monoid_algebra): the distrib_mul_action (#2417)

kim-em committed 5 years ago

51e03aad

chore(category_theory/opposites): typo fix (#2466)

b-mehta committed 5 years ago

036b0386

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

leanprover-community-bot committed 5 years ago

59a767ee

feat(category_theory/opposites): some opposite category properties (#2464)

b-mehta committed 5 years ago

44743821

fix(tactic/delta_instance): handle universe metavariables (#2463)

kim-em committed 5 years ago

58088cc9

fix(category_theory/limits): avoid a rewrite in a definition (#2458)

TwoFX committed 5 years ago

9b255781

chore(tactic/simp_result): forgot to import in tactic.basic (#2462)

kim-em committed 5 years ago

c0afa80e

fix(category_theory/limits): make image.map_comp a simp lemma (#2456)

TwoFX committed 5 years ago

a8edb5e2

fix(category_theory/limits): remove an unnecessary axiom in has_image_map (#2455)

TwoFX committed 5 years ago

e6aa533b

feat(category_theory/eq_to_iso): missing simp lemma (#2454)

kim-em committed 5 years ago

aa55f8b5

feat(continued_fractions) add stabilisation under termination lemmas (#2451)

kappelmann committed 5 years ago

9801c1c0

chore(number_theory/sum_four_squares): slightly shorten proof (#2457)

ChrisHughes24 committed 5 years ago

6054f7c9

chore(category_theory/monoidal): some arguments that need to be made explicit in 3.8

kim-em committed 5 years ago

d344310e

Newer Older