mathlib3

7e350c24 - feat(category_theory/*): Fully faithful functors induces equivalence (#9322)

feat(category_theory/*): Fully faithful functors induces equivalence (#9322) Needed for AffineSchemes ≌ CommRingᵒᵖ. Co-authored-by: erdOne <36414270+erdOne@users.noreply.github.com>