PR #1937 feat(data/fintype): range_prod_eq_univ_prod

feat(data/fintype): range_prod_eq_univ_prod #1937

mergify merged 6 commits into master from range-prod-eq-univ-prod

feat(algebra/big_operators): range_prod_eq_univ_prod

38b9aac5

fix build, part 1

f13db1d8

fix build, part 2

4264b02e

jcommelin changed the title ~~feat(algebra/big_operators): range_prod_eq_univ_prod~~ feat(data/fintype): range_prod_eq_univ_prod 6 years ago

fix build, part 3

164f1d22

Fix build, part 4

fb0f88ec

urkud approved these changes on 2020-02-01

urkud added ready-to-merge

Merge branch 'master' into range-prod-eq-univ-prod

70cd717e

mergify merged 11b94970 into master 6 years ago

mergify deleted the range-prod-eq-univ-prod branch 6 years ago

Reviewers

urkud

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone