mathlib3
chore(*): completing most of the -T50000 challenge
#2281

Merged

chore(*): completing most of the -T50000 challenge #2281

mergify merged 2 commits into master from T50000-challenge

chore(*): completing most of the -T50000 challenge

3e500a94

bryangingechen approved these changes on 2020-03-30

bryangingechen added ready-to-merge

Merge branch 'master' into T50000-challenge

ffb86635

mergify merged 1331e29b into master 5 years ago

robertylewis deleted the T50000-challenge branch 5 years ago

Reviewers

bryangingechen

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone