mathlib
mathlib copied to clipboard
feat(category_theory/limits): has_limits_of_shape J if and only if const J is a left adjoint
This PR/issue depends on:
- ~~leanprover-community/mathlib#15796~~
- ~~leanprover-community/mathlib#15797~~
- ~~leanprover-community/mathlib#15858~~ By Dependent Issues (🤖). Happy coding!
bors merge p=4
Pull request successfully merged into master.
Build succeeded: