mathlib3
4b6ec60f - lint(topology/algebra/order/basic): use `finite` instead of `fintype` (#15203)

Commit

3 years ago

lint(topology/algebra/order/basic): use `finite` instead of `fintype` (#15203)

Author

urkud

urkud

Parents

Loading