leanprover-community/mathlib

Pull Requests Commits

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

bryangingechen committed 6 years ago

0f6b3ca4

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

leanprover-community-bot committed 6 years ago

96676a76

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

urkud committed 6 years ago

4ec7cc58

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

sgouezel committed 6 years ago

338bbd20

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

leanprover-community-bot committed 6 years ago

593f731d

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

leanprover-community-bot committed 6 years ago

5444945d

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

sgouezel committed 6 years ago

f71e3597

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

jcommelin committed 6 years ago

9a7151c7

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

urkud committed 6 years ago

666b9e59

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

jcommelin committed 6 years ago

257d1b7c

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

pechersky committed 6 years ago

447a2d6c

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

ChrisHughes24 committed 6 years ago

1df93013

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

urkud committed 6 years ago

ce48b6ba

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

kckennylau committed 6 years ago

cf0c6b83

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

urkud committed 6 years ago

5129aed5

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

leanprover-community-bot committed 6 years ago

ade196f8

feat(ring_theory/ideals): prod_dvd_of_coprime (#2815)

kl-i committed 6 years ago

8863666a

feat(linear_algebra/matrix): matrix has finite dim (#3013)

pechersky committed 6 years ago

2779093b

chore(*): update to lean 3.16.1c (#3020)

bryangingechen committed 6 years ago

067a96b7

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

leanprover-community-bot committed 6 years ago

76e7d298

feat(tactic/generalizes): tactic for generalizing over multiple expressions (#2982)

JLimperg committed 6 years ago

f7654b3f

style(*): use rcases patterns with ext (#3018)

robertylewis committed 6 years ago

daed8a41

ci(build.yml): add -T100000 to test step (#3017)

bryangingechen committed 6 years ago

026d639f

chore(*): update to lean 3.16.0 (#3016)

gebner committed 6 years ago

614d1cad

chore(algebra/field): deduplicate with group_with_zero (#3015)

urkud committed 6 years ago

4b622613

chore(data/equiv/basic): add many docstrings, review (#3008)

urkud committed 6 years ago

b427ebf9

feat(control/equiv_functor/instances): allow equiv_rw on finset (#2997)

kim-em committed 6 years ago

671284e3

feat(data/set/function): add lemmas about `semiconj` (#3007)

urkud committed 6 years ago

b932a510

chore(*): use sum notation (#3014)

kckennylau committed 6 years ago

836c0a26

feat(linear_algebra/basic): curry is linear_equiv (#3012)

pechersky committed 6 years ago

d9934b26

Newer Older