leanprover-community/mathlib

Pull Requests Commits
feat(category_theory): add naturality_assoc simp lemma (#2200)
kim-em committed 6 years ago
Verified 34bac8d3
chore(category_theory): change monoidal_of_has_finite_products to use binary products (#2190)
kim-em committed 6 years ago
Verified 99ba8f44
feat(category_theory): unbundled functors and lax monoidal functors (#2193)
kim-em committed 6 years ago
Verified 94201677
chore(scripts): update nolints.txt
leanprover-community-bot committed 6 years ago
b224943d
feat(finsupp): move convolution product to type wrapper `add_monoid_algebra`. (#2135)
kim-em committed 6 years ago
Verified 8d44098d
feat(category_theory/limits): the isomorphism expressing preservation of chosen limits (#2192)
kim-em committed 6 years ago
Verified 0f1b4654
chore(algebra/Module/monoidal): add the simp lemmas for unitors and associativity (#2196)
kim-em committed 6 years ago
Verified c66c4afa
chore(category_theory): missing simp lemmas (#2188)
kim-em committed 6 years ago
Verified d93e0ddb
feat(category_theory): subsingleton (has_zero_morphisms) (#2180)
kim-em committed 6 years ago
Verified b4e6313a
chore(scripts): update nolints.txt
leanprover-community-bot committed 6 years ago
cc041325
feat(category_theory): some natural isomorphisms related to composition by functors (#2189)
kim-em committed 6 years ago
Verified 6c97ce02
feat(data/zmod): lemmas about totient and zmod (#2158)
ChrisHughes24 committed 6 years ago
Verified d12bbc00
oh dear
kim-em committed 6 years ago
2d371ceb
chore(scripts): update nolints.txt
leanprover-community-bot committed 6 years ago
3dd95a2e
Merge branch 'monoidal_of_has_finite_products' into enriched
kim-em committed 6 years ago
6d1313bb
docs(category_theory/limits): adding many docstrings (#2185)
kim-em committed 6 years ago
Verified 1a398a72
fixes
kim-em committed 6 years ago
183bf7b4
Merge branch 'concrete_no_extend' into enriched
kim-em committed 6 years ago
c3693ae7
Merge branch 'monoidal_of_has_finite_products' into enriched
kim-em committed 6 years ago
2793c942
chore(category_theory/concrete_category): take an instance, rather than extending, category
kim-em committed 6 years ago
1961b61f
remove some simp annotations for now
kim-em committed 6 years ago
a628bb59
feat(data/finset): monotone bijection from fin k (#2163)
sgouezel committed 6 years ago
Verified 344a41e8
back out independent changes which have been moved to other PRs
kim-em committed 6 years ago
2eb875cc
merge
kim-em committed 6 years ago
aa9194e6
feat(category_theory/limits): the isomorphism expressing preservation of chosen limits
kim-em committed 6 years ago
6ed879c3
Merge branch 'pair_comp' into enriched
kim-em committed 6 years ago
6e3c90d3
better design
kim-em committed 6 years ago
2c4882b1
merge
kim-em committed 6 years ago
8c8a5fcd
fix
kim-em committed 6 years ago
cea46ce4
merge
kim-em committed 6 years ago
61fc8612
Terms Of Use Privacy Policy Refund Policy Impressum