mathlib
41c7b1e3 - chore(category_theory/Fintype): remove redundant lemmas (#7531)

Commit

4 years ago

chore(category_theory/Fintype): remove redundant lemmas (#7531) These lemmas exist for arbitrary concrete categories. - [x] depends on: #7530

Author

jcommelin

Parents