mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard

feat(category_theory/limits): has_limits_of_shape J if and only if const J is a left adjoint

Open TwoFX opened this issue 2 years ago • 1 comments


  • [x] depends on: #15796
  • [x] depends on: #15797
  • [x] depends on: #15858

Open in Gitpod

TwoFX avatar Aug 04 '22 08:08 TwoFX

This PR/issue depends on:

  • ~~leanprover-community/mathlib#15796~~
  • ~~leanprover-community/mathlib#15797~~
  • ~~leanprover-community/mathlib#15858~~ By Dependent Issues (🤖). Happy coding!

Build failed (retrying...):

bors[bot] avatar Aug 15 '22 15:08 bors[bot]

Build failed (retrying...):

bors[bot] avatar Aug 15 '22 16:08 bors[bot]

Build failed (retrying...):

bors[bot] avatar Aug 15 '22 16:08 bors[bot]

bors merge p=4

jcommelin avatar Aug 15 '22 19:08 jcommelin

Build failed (retrying...):

bors[bot] avatar Aug 15 '22 22:08 bors[bot]

Pull request successfully merged into master.

Build succeeded:

bors[bot] avatar Aug 16 '22 10:08 bors[bot]