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

feat(data/fintype/card): prod_univ_sum

ChrisHughes24 committed 5 years ago

Update src/data/fintype.lean

sgouezel committed 5 years ago

Update src/data/fintype/card.lean

sgouezel committed 5 years ago

docstrings

ChrisHughes24 committed 5 years ago

fix build

ChrisHughes24 committed 5 years ago

remove unused argument

ChrisHughes24 committed 5 years ago

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

ChrisHughes24 committed 5 years ago

fix build

ChrisHughes24 committed 5 years ago

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

bryangingechen committed 5 years ago

Merge branch 'master' into prod_univ_sum

mergify[bot] committed 5 years ago

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