Commit 2021-05-10 13:15 41c7b1e3
View on Github →chore(category_theory/Fintype): remove redundant lemmas (#7531) These lemmas exist for arbitrary concrete categories.
- depends on: #7530
chore(category_theory/Fintype): remove redundant lemmas (#7531) These lemmas exist for arbitrary concrete categories.