mathlib3
feat(topology/subset_properties): fintype.compact_space
#1786

Merged

feat(topology/subset_properties): fintype.compact_space #1786

mergify merged 2 commits into master from jcommelin-patch-3

feat(topology/subset_properties): fintype.compact_space

ec00d561

PatrickMassot approved these changes on 2019-12-06

PatrickMassot added ready-to-merge

sgouezel commented on 2019-12-06

Merge branch 'master' into jcommelin-patch-3

4099ae93

mergify merged 8ca92637 into master 6 years ago

mergify deleted the jcommelin-patch-3 branch 6 years ago

Reviewers

PatrickMassot

sgouezel

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone