leanprover-community/mathlib3

Pull Requests Commits

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

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

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

feat(logic/nontrivial): function.injective.exists_ne (#3983)

jsm28 committed 5 years ago

1073204e

feat(meta/widget): Add css classes for indentation as required by group and nest. (#3764)

DanielFabian committed 5 years ago

942c779d

feat(data/complex/is_R_or_C): add typeclass for real or complex (#3934)

dupuisf committed 5 years ago

ffce8f67

feat(set_theory/game): computation of grundy_value (nim n + nim m) (#3977)

TwoFX committed 5 years ago

a18f142d

feat(data/fin): nontrivial instance (#3979)

jsm28 committed 5 years ago

dfdb38ab

feat(linear_algebra/char_poly/coeff,*): prerequisites for friendship theorem (#3953)

jalex-stark committed 5 years ago

14e7fe83

feat(linear_algebra): determinant of vectors in a basis (#3919)

PatrickMassot committed 5 years ago

4c4243c5

doc(topology/sheaves): update module docs (#3971)

kim-em committed 5 years ago

94b1292f

feat(data/nat): API for test_bit and bitwise operations (#3964)

TwoFX committed 5 years ago

ba41f0a4

chore(topology/sheaves/sheaf_of_functions): rely less on defeq (#3972)

kim-em committed 5 years ago

faf1df48

chore(*): bump to lean 3.19.0c, fin is now a subtype (#3955)

jcommelin committed 5 years ago

fd4628f1

feat(algebraic_geometry): structure sheaf on Spec R (#3907)

kim-em committed 5 years ago

17c4651c

refactor(set_theory/game): make impartial a class (#3974)

TwoFX committed 5 years ago

84d47a0f

feat(analysis/convex): add correspondence between convex cones and ordered semimodules (#3931)

dupuisf committed 5 years ago

ea177c2a

chore(algebra/group_with_zero): adjust some instance priorities (#3968)

rwbarton committed 5 years ago

53275f49

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

leanprover-community-bot committed 5 years ago

2d3530d5

Newer Older