leanprover-community/mathlib3

Pull Requests Commits

feat(category_theory/limits): the universal morphism colim_j lim_k F(j,k) -> lim_k colim_j F(j,k)

kim-em committed 5 years ago

03bc30fb

feat(geometry/euclidean/circumcenter): more lemmas (#4028)

jsm28 committed 5 years ago

dd633c28

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

leanprover-community-bot committed 5 years ago

c86359f7

fix(docs/100.yaml): fix indentation in 100 list (#4029)

Qian Hong committed 5 years ago

ca5703d5

fix(test/*): make sure tests produce no output (#3947)

fpvandoorn committed 5 years ago

7b9db99c

feat(order/rel_iso): define `rel_hom` (relation-preserving maps) (#3946)

awainverse committed 5 years ago

9d42f6c6

feat(linear_algebra/affine_space): more lemmas (#3990)

jsm28 committed 5 years ago

57463fa4

chore(topology/sheaves): depend less on rfl (#3994)

kim-em committed 5 years ago

71ef45e2

chore(algebra/category/CommRing/limits): don't use deprecated.subring (#4010)

kim-em committed 5 years ago

895f6ee7

chore(data/fin): succ_above defn compares fin terms instead of values (#3999)

pechersky committed 5 years ago

ddbdfeb5

feat(ring_theory/localization): Localizations of integral extensions (#3942)

dtumad committed 5 years ago

96c80e24

feat(linear_algebra/eigenspace): add generalized eigenspaces (#4015)

abentkamp committed 5 years ago

cd36773a

feat(field_theory/adjoin): adjoining elements to fields (#3913)

tb65536 committed 5 years ago

7310eab9

feat(ring_theory/localization): localization away from an element (#4019)

101damnations committed 5 years ago

8026ea8a

feat(pfun/recursion): unbounded recursion (#3778)

cipher1024 committed 5 years ago

0b4444ca

doc(slim_check): improve documentation, swap instances (#4023)

cipher1024 committed 5 years ago

d94643c5

feat(slim_check/errors): improve error messages and add useful instances (#4022)

cipher1024 committed 5 years ago

ef22a33f

feat(testing): property based testing (basics) (#3915)

cipher1024 committed 5 years ago

0c2e77c9

feat(analysis/calculus/times_cont_diff): iterated smoothness in terms of deriv (#4017)

sgouezel committed 5 years ago

329393a7

feat(docs,ci): move overview, undergrad, and 100 theorems lists from website (#4016)

robertylewis committed 5 years ago

849a5f9b

refactor(algebra/category/*, category_theory/concrete_category): generalize universes for concrete categories (#3687)

TwoFX committed 5 years ago

6a5241f2

feat(data/mv_polynomial): assorted lemmas (#4002)

robertylewis committed 5 years ago

a97d71b5

feat(archive/100-theorems-list): friendship theorem (nr 83) (#3970)

jalex-stark committed 5 years ago

2688d42b

chore(*): more use of bundled ring homs (#4012)

kim-em committed 5 years ago

12763ecc

chore(ring_theory/free_ring): use bundled ring homs (#4011)

kim-em committed 5 years ago

51546d29

chore(algebraic_geometry/Spec): reduce imports (#4007)

kim-em committed 5 years ago

93468fee

refactor(algebra/associates): unite `associates.prime` with `prime` (#3988)

awainverse committed 5 years ago

551cf8e2

feat(category_theory/limits/shapes/terminal): is_terminal object (#3957)

b-mehta committed 5 years ago

7cd67b56

feat(data/{finset,finsupp,multiset}): more assorted lemmas (#4006)

robertylewis committed 5 years ago

fc57cf49

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

leanprover-community-bot committed 5 years ago

c33b41b0

Older