Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-23 23:56 bf6cd285

View on Github →

feat(category_theory/fully_faithful): equivalence of homsets (#3923) I was so sure I'd already made this PR but I can't find it nor this construction, so here it is.

Estimated changes