leanprover-community/mathlib3

Pull Requests Commits

kim-em committed 4 years ago

e81fcf97

works ... a bit too well

kim-em committed 5 years ago

54544a9b

kim-em committed 5 years ago

db67c733

kim-em committed 5 years ago

7e908466

chore(*): update to Lean 3.16.2c (#3053)

bryangingechen committed 5 years ago

51ad2a18

feat(linear_algebra/affine_space): define a few affine maps (#2981)

urkud committed 5 years ago

ce594be5

feat(data/*): lemmas converting finset, set.finite, and their card (#3042)

pechersky committed 5 years ago

14292790

fix(library_search): only unfold reducible definitions when matching (#3038)

kim-em committed 5 years ago

c955537e

chore(*): remove extra author info (#3051)

pechersky committed 5 years ago

5c0000c0

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

leanprover-community-bot committed 5 years ago

64461b83

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

leanprover-community-bot committed 5 years ago

6aa24643

chore(data/complex/exponential): linting and pp_nodot (#3045)

bryangingechen committed 5 years ago

f78693db

feat(analysis/mean_inequalities): Holder and Minkowski inequalities (#3025)

urkud committed 5 years ago

5808afcb

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

leanprover-community-bot committed 5 years ago

27a09466

chore(data/real/cau_seq): linting (#3040)

bryangingechen committed 5 years ago

30e620ce

doc(data/complex/basic): docstrings and pp_nodots (#3044)

bryangingechen committed 5 years ago

0f6b3ca4

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

leanprover-community-bot committed 5 years ago

96676a76

refactor(*): fix field names in `linear_map` and `submodule` (#3032)

urkud committed 5 years ago

4ec7cc58

chore(measure/theory): remove useless module instances (#3031)

sgouezel committed 5 years ago

338bbd20

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

leanprover-community-bot committed 5 years ago

593f731d

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

leanprover-community-bot committed 5 years ago

5444945d

chore(ring_theory/power_series): avoid id in instances (#3033)

sgouezel committed 5 years ago

f71e3597

feat(data/finsupp): set.finite {m | m ≤ n} (#3029)

jcommelin committed 5 years ago

9a7151c7

refactor(analysis/mean_inequalities): review (#3023)

urkud committed 5 years ago

666b9e59

feat(*): preparations for Caratheodory's convexity theorem (#3030)

jcommelin committed 5 years ago

257d1b7c

chore(data/matrix/basic): move numeral section into diagonal (#3022)

pechersky committed 5 years ago

447a2d6c

feat(group_theory/semidirect_product): introduce semidirect_products of groups (#3028)

ChrisHughes24 committed 5 years ago

1df93013

chore(data/finsupp): drop `finsupp.module` and `vector_space` (#3009)

urkud committed 5 years ago

ce48b6ba

chore(*): use prod and sum notation (#3027)

kckennylau committed 5 years ago

cf0c6b83

chore(algebra/group/to_additive): improve warning message (#3024)

urkud committed 5 years ago

5129aed5

Older