leanprover-community/mathlib3

Pull Requests Commits

adamtopaz committed 5 years ago

28374d45

adamtopaz committed 5 years ago

3f8f696e

Add localization.lean

adamtopaz committed 5 years ago

30a1f2c1

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

leanprover-community-bot committed 5 years ago

7271f74f

feat(system/random): a monad for (pseudo-)randomized computations (#3742)

cipher1024 committed 5 years ago

0a48f0a2

feat(linear_algebra): some easy linear map/equiv lemmas (#3890)

PatrickMassot committed 5 years ago

36386fc7

chore(data/matrix, linear_algebra): generalize universe parameters (#3879)

Vierkantor committed 5 years ago

c9704ff5

feat(ring_theory/separable): a separable polynomial splits into a product of unique `X - C a` (#3877)

Vierkantor committed 5 years ago

901c5bca

chore(category_theory/limits/types): cleanup (#3871)

kim-em committed 5 years ago

9f525c74

doc(src/ring_theory/integral_domain.lean): add module docstring (#3881)

kbuzzard committed 5 years ago

7a93d87c

feat(data/polynomial): Add polynomial/eval lemmas (#3876)

abentkamp committed 5 years ago

46310185

feat(equiv/transfer_instances): other algebraic structures (#3870)

kim-em committed 5 years ago

e174f42c

feat(data/list/basic): lemmas about foldr/foldl (#3865)

abentkamp committed 5 years ago

d7621b93

chore(data/complex/module): move `linear_map.{re,im,of_real}` from `analysis` (#3874)

urkud committed 5 years ago

ba06edc1

feat(order/category): various categories of ordered types (#3841)

jcommelin committed 5 years ago

34db3c34

fix(data/fin): better defeqs in fin.has_le instance (#3869)

digama0 committed 5 years ago

43647988

feat(linear_algebra/affine_space/basic): more direction lemmas (#3867)

jsm28 committed 5 years ago

9a8e504a

feat(linear_algebra/affine_space/basic): more vector_span lemmas (#3866)

jsm28 committed 5 years ago

7e6b8a9d

feat(ring_theory/polynomial/basic): Isomorphism between polynomials over a quotient and quotient over polynomials (#3847)

dtumad committed 5 years ago

bd5552a3

feat(analysis/normed_space/real_inner_product): orthogonal subspace order (#3863)

jsm28 committed 5 years ago

15cacf0e

refactor(algebra/add_torsor,linear_algebra/affine_space/basic): vsub_set (#3858)

jsm28 committed 5 years ago

d963213b

chore(data/finset/basic): use `finset.map` in `sigma_eq_bind` (#3857)

urkud committed 5 years ago

1e677e66

doc(linear_algebra/sesquilinear_form): add missing backtick (#3862)

gebner committed 5 years ago

a1003964

fix(test/norm_cast): fix(?) test (#3859)

kbuzzard committed 5 years ago

8579a5f7

feat(analysis/calculus) : L'Hôpital's rule, 0/0 case (#3740)

ADedecker committed 5 years ago

425aee91

feat(miu_language): a formalisation of the MIU language described by D. Hofstadter in "Gödel, Escher, Bach". (#3739)

gihanmarasingha committed 5 years ago

5d2256da

chore(algebra/euclidean_domain): docstrings (#3816)

ChrisHughes24 committed 5 years ago

0854e839

chore(logic/basic): `and_iff_left/right_iff_imp`, `or.right_comm` (#3854)

urkud committed 5 years ago

78770333

doc(field_theory/tower): correct docstring (#3853)

kckennylau committed 5 years ago

cb4a5a24

feat(data/option/basic): add ne_none_iff_exists (#3856)

kbuzzard committed 5 years ago

9a705331

Older