mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat: target of final functor is connected iff source is connected

Open datokrat opened this issue 1 year ago • 3 comments

This PR is part of the effort to prove the Freyd-Mitchell embedding theorem.

Open in Gitpod

datokrat avatar Feb 25 '24 22:02 datokrat

Hi, for PRs that build on other PRs, we usually have the later PR (in your case, this one) also have master as the target branch, but record the dependency in the PR description. The syntax is explained if you edit the PR description. A bot wil then add the blocked-by-other-PR label after a few minutes.

TwoFX avatar Feb 27 '24 06:02 TwoFX

I think it's okay to make the PR point to a dependent branch in order to reduce diffs, making it immediately reviewable without using another link, but you'd better change the target branch to master before the dependent PR is merged: otherwise GitHub will automatically close this PR once the target branch is merged, and you'll have to restore that branch in order to reopen it and change the target branch.

alreadydone avatar Feb 27 '24 16:02 alreadydone

Thanks for the hints! I'll change the target for now.

datokrat avatar Mar 01 '24 20:03 datokrat

Thanks!

bors merge

joelriou avatar May 28 '24 21:05 joelriou

Pull request successfully merged into master.

Build succeeded:

mathlib-bors[bot] avatar May 28 '24 21:05 mathlib-bors[bot]