mathlib3
bf6cd285 - feat(category_theory/fully_faithful): equivalence of homsets (#3923)

Commit

5 years ago

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.

References

#4925 - Make prime-avoidance branch build

Author

b-mehta

Parents

7d4f7730

mathlib3 bf6cd285 - feat(category_theory/fully_faithful): equivalence of homsets (#3923)

mathlib3
bf6cd285 - feat(category_theory/fully_faithful): equivalence of homsets (#3923)