mathlib3

292fc042 - feat(category_theory): adjunction convenience defs (#2754)

feat(category_theory): adjunction convenience defs (#2754) Transport adjunctions along natural isomorphisms, and `is_left_adjoint` or `is_right_adjoint` versions of existing adjunction properties.