PR #2284 feat(data/fintype/card): prod_univ_sum

feat(data/fintype/card): prod_univ_sum #2284

mergify merged 10 commits into master from prod_univ_sum

feat(data/fintype/card): prod_univ_sum

d2126600

sgouezel approved these changes on 2020-03-29

Update src/data/fintype.lean

a599607c

Update src/data/fintype/card.lean

bc7e2291

sgouezel added ready-to-merge

urkud commented on 2020-03-29

sgouezel removed ready-to-merge

docstrings

48f91f3a

urkud added ready-to-merge

fix build

a8e71a11

remove unused argument

0e8181bd

Merge remote-tracking branch 'origin/master' into prod_univ_sum

05683561

fix build

09467491

Merge remote-tracking branch 'community/master' into prod_univ_sum

179bf437

Merge branch 'master' into prod_univ_sum

d246757d

mergify merged 7d89f2ea into master 5 years ago

ChrisHughes24 deleted the prod_univ_sum branch 5 years ago

Reviewers

sgouezel

urkud

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone