mathlib
b7864434 - chore(algebra/category/*): Added `of_hom` to all of the algebraic categories. (#9454)

Commit
4 years ago
chore(algebra/category/*): Added `of_hom` to all of the algebraic categories. (#9454) As suggested in the comments of #9416.
Author
Parents
Loading