leanprover-community/mathlib3

Pull Requests Commits

feat(algebra/big-operators): some big operator lemmas (#2152)

b-mehta committed 6 years ago

fe878eaf

feat(data/finset): finset lemmas from combinatorics (#2149)

b-mehta committed 6 years ago

67e363fd

feat(combinatorics/composition): introduce compositions of an integer (#2398)

sgouezel committed 6 years ago

f3ac7b70

feat(category_theory/limits/shapes/binary_products): add some basic API for prod and coprod (#2396)

kbuzzard committed 6 years ago

01ac691d

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

leanprover-community-bot committed 6 years ago

cf89963e

refactor(order/filter): refactor filters infi and bases (#2384)

PatrickMassot committed 6 years ago

17b2d065

feat(algebra/homology): the cohomology functor (#2374)

TwoFX committed 6 years ago

92c8d93d

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

leanprover-community-bot committed 6 years ago

ca986598

chore(algebra/module): rename type vars, minor cleanup, add module docstring (#2392)

urkud committed 6 years ago

51f7319b

chore(*): futureproof import syntax (#2402)

rwbarton committed 6 years ago

64fa9a20

feat(category_theory): biproducts, and biproducts in AddCommGroup (#2187)

kim-em committed 6 years ago

ef4d2354

fix(tactic/norm_cast): typo (#2400)

kbuzzard committed 6 years ago

1433f051

feat(set_theory/game): short games, boards, and domineering (#1540)

kim-em committed 6 years ago

d84de804

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

leanprover-community-bot committed 6 years ago

0f893920

feat(category_theory): functorial images (#2373)

TwoFX committed 6 years ago

ee8cb15a

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

leanprover-community-bot committed 6 years ago

aa42f3b4

chore(tactic/lean_core_docs): add API docs for core Lean tactics (#2371)

kbuzzard committed 6 years ago

5f1bfcf2

feat(category_theory): define action_category (#2358)

dwarn committed 6 years ago

80340d83

refactor(*): rename ordered groups/monoids to ordered add_ groups/monoids (#2347)

jcommelin committed 6 years ago

e1feab4e

chore(algebra/category): remove some [reducible] after Lean 3.8 (#2389)

kim-em committed 6 years ago

c9fca154

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

leanprover-community-bot committed 6 years ago

83359d14

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

leanprover-community-bot committed 6 years ago

4fa29249

feat(actions): manage labels on PR review (#2387)

bryangingechen committed 6 years ago

81d8104f

chore(category_theory/types): add documentation, remove bad simp lemmas and instances, add notation for functions as morphisms (#2383)

kim-em committed 6 years ago

c68f23df

perf(data/*): add inline attributes (#2380)

jcommelin committed 6 years ago

00b510eb

fix(tactic/equiv_rw): don't use `subst` unnecessarily (#2334)

kim-em committed 6 years ago

690643ab

feat(category_theory): make defining groupoids easier (#2360)

dwarn committed 6 years ago

8556499f

chore(*): switch to lean 3.8.0 (#2361)

gebner committed 6 years ago

597704ac

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

leanprover-community-bot committed 6 years ago

ebdeb3b6

feat(data/list/range): add sum lemmas (#2385)

kbuzzard committed 6 years ago

29080c8c

Newer Older