leanprover-community/mathlib

Pull Requests Commits

Scott Morrison committed 5 years ago

b7d2f521

Scott Morrison committed 5 years ago

2117a4d5

leaving a comment for the future

Scott Morrison committed 5 years ago

ed3b8c41

feat(logic/basic): a few simp lemmas about `and` and `or` (#2408)

ChrisHughes24 committed 5 years ago

8356b798

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

b-mehta committed 5 years ago

fe878eaf

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

b-mehta committed 5 years ago

67e363fd

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

sgouezel committed 5 years ago

f3ac7b70

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

kbuzzard committed 5 years ago

01ac691d

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

leanprover-community-bot committed 5 years ago

cf89963e

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

PatrickMassot committed 5 years ago

17b2d065

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

TwoFX committed 5 years ago

92c8d93d

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

leanprover-community-bot committed 5 years ago

ca986598

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

urkud committed 5 years ago

51f7319b

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

rwbarton committed 5 years ago

64fa9a20

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

kim-em committed 5 years ago

ef4d2354

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

kbuzzard committed 5 years ago

1433f051

Scott Morrison committed 5 years ago

c92fda20

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

kim-em committed 5 years ago

d84de804

oops, one more long line

Scott Morrison committed 5 years ago

aa928434

Scott Morrison committed 5 years ago

ccdaef06

Merge branch 'domineering' of github.com:leanprover-community/mathlib into domineering

Scott Morrison committed 5 years ago

663a552f

Apply suggestions from code review

kim-em committed 5 years ago

Verified 79b5fa69

Merge remote-tracking branch 'origin/master' into domineering

Scott Morrison committed 5 years ago

b1c45069

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

leanprover-community-bot committed 5 years ago

0f893920

feat(category_theory): functorial images (#2373)

TwoFX committed 5 years ago

ee8cb15a

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

leanprover-community-bot committed 5 years ago

aa42f3b4

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

kbuzzard committed 5 years ago

5f1bfcf2

feat(category_theory): define action_category (#2358)

dwarn committed 5 years ago

80340d83

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

jcommelin committed 5 years ago

e1feab4e

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

kim-em committed 5 years ago

c9fca154

Older