Commit 2022-07-24 16:34 aed4c494
View on Github →refactor(data/{finite,fintype}): move some lemmas to data.fintype.basic (#15626)
We should have lemmas like nonempty_fintype in fintype.basic to replace [fintype _] by [finite _] in the assumptions. This PR doesn't fix any assumptions to keep it small.