mathlib3
d38aca11 - chore(topology/*): Use `finite` in place of `fintype` where possible (#15891)

Commit

3 years ago

chore(topology/*): Use `finite` in place of `fintype` where possible (#15891) Satisfy the `fintype_finite` linter.

Author

YaelDillies

Parents