leanprover-community/mathlib3

Pull Requests Commits

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

feat(category_theory/monoidal/internal): Mon_ (Module R) ≌ Algebra R (#3695)

kim-em committed 5 years ago

e053bdab

feat(linear_algebra/finite_dimensional): eq_of_le_of_findim_eq (#4005)

jsm28 committed 5 years ago

036527ae

feat(analysis/normed_space/real_inner_product): inner_add_sub_eq_zero_iff (#4004)

jsm28 committed 5 years ago

be3b1758

feat(analysis/special_functions/trigonometric): ranges of `real.sin` and `real.cos` (#3998)

ADedecker committed 5 years ago

d0a8cc4b

fix(widget): workaround for webview rendering bug (#3997)

EdAyers committed 5 years ago

d4484a4e

feat(algebra/field, ring_theory/ideal/basic): an ideal is maximal iff the quotient is a field (#3986)

AlexandruBosinta committed 5 years ago

d2b18a18

chore(category_theory/limits): some simp lemmas (#3993)

kim-em committed 5 years ago

8089f506

feat(data/fin): simplify fin.mk (#3996)

jsm28 committed 5 years ago

9e9e318c

feat(measure_theory): induction principles in measure theory (#3978)

fpvandoorn committed 5 years ago

10ebb718

Newer Older