leanprover-community/mathlib

Pull Requests Commits

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

Merge branch 'computability' into computability-list

pimsp committed 5 years ago

ece5f0dc

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

AlexandruBosinta committed 5 years ago

d2b18a18

Put everything in namespace computability to avoid cluttering root namespace

pimsp committed 5 years ago

a63c3bd5

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

kim-em committed 5 years ago

8089f506

Replaced sorry with proofs and added evals_to.refl and .trans

pimsp committed 5 years ago

8cd3cb4d

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

fix(algebraic_geometry/Spec): inline TeX in heading (#3992)

bryangingechen committed 5 years ago

bf7487b5

feature(algebraic_geometry/Scheme): the category of schemes (#3961)

kim-em committed 5 years ago

b79fc037

feat(data/finset/sort): range_mono_of_fin (#3987)

jsm28 committed 5 years ago

e88843ca

Refactored equality of alphabets to equivalence of alphabets

pimsp committed 5 years ago

543c122f

feat(widget): add go to definition button. (#3982)

EdAyers committed 5 years ago

861f1821

feat(topology/tactic): optionally make `continuity` verbose with `?` (#3962)

Jesse Michael Han committed 5 years ago

f9ee4166

Newer Older