leanprover-community/mathlib

Pull Requests Commits
Merge remote-tracking branch 'origin/master' into enriched
kim-em committed 6 years ago
2d25598c
fixes
kim-em committed 6 years ago
554a33bc
chore(category_theory): remove functor.of (#2127)
kim-em committed 6 years ago
Verified 43431be5
fix(algebra/category): avoid deprecated lemmas (#2126)
kim-em committed 6 years ago
Verified d909a612
fix import
kim-em committed 6 years ago
7095bb23
remove obsolete comment
kim-em committed 6 years ago
df5b743d
merge
kim-em committed 6 years ago
4fe1b488
tweaks
kim-em committed 6 years ago
6c9166ed
minor
kim-em committed 6 years ago
eadb5587
docstrings
kim-em committed 6 years ago
6a2fc6f9
feat(algebra): monoidal category of R-modules
kim-em committed 6 years ago
2806d684
Merge remote-tracking branch 'origin/master' into enriched
kim-em committed 6 years ago
fe818f3a
minor
kim-em committed 6 years ago
ccc3e032
yay, monoidal category of R-Mod
kim-em committed 6 years ago
de4733c0
Add two missing duals (#2122)
TwoFX committed 6 years ago
Verified 36ac9162
various
kim-em committed 6 years ago
6830ae7d
feat(ci): look for equivalent oleans on Azure (#2094)
robertylewis committed 6 years ago
Verified 699401bc
merge
kim-em committed 6 years ago
dd686e4d
merge
kim-em committed 6 years ago
bdd59c0e
removing defunct colimits
kim-em committed 6 years ago
5839b3f4
feat(measurable_space): is_measurable_supr lemma (#2092)
kim-em committed 6 years ago
Verified 668a98e7
feat(ring_theory/polynomial): refactor of is_integral_domain_fin (#2119)
kim-em committed 6 years ago
Verified 9feefee8
feat(analysis/calculus/tangent_cone): prove that all intervals are `unique_diff_on` (#2108)
urkud committed 6 years ago
Verified cdc56baf
feat(category_theory/limits): the pullback of a monomorphism is a monomorphism (#2113)
TwoFX committed 6 years ago
Verified e8ad2e38
feat(linter): include linter name in report (#2116)
robertylewis committed 6 years ago
Verified 945845d8
chore(ring_theory/polynomial): refactor proof of is_noetherian_ring_fin (#2117)
kim-em committed 6 years ago
Verified 4089712f
reflexive transitive closure is symmetric of original (#2115)
b-mehta committed 6 years ago
Verified 25df8842
feat(algebra/group/hom): cancel injective/surjective `monoid_hom`s (#2112)
urkud committed 6 years ago
Verified f90803c9
feat(analysis/calculus/darboux): IVT for derivatives (#2110)
urkud committed 6 years ago
Verified b39713fe
feat(category_theory): images (#2100)
kim-em committed 6 years ago
Verified 62abc4d5
Terms Of Use Privacy Policy Refund Policy Impressum