Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - feat(algebra/module/projective): projective modules are closed under product #16735

Closed
wants to merge 5 commits into from
Closed

[Merged by Bors] - feat(algebra/module/projective): projective modules are closed under product #16735

wants to merge 5 commits into from

Conversation

antoinelab01
Copy link
Collaborator

Open in Gitpod

@antoinelab01 antoinelab01 added awaiting-review The author would like community review of the PR t-algebra Algebra (groups, rings, fields etc) labels Sep 30, 2022
@antoinelab01 antoinelab01 mentioned this pull request Oct 1, 2022
Closed
1 task
tb65536
tb65536 reviewed Oct 1, 2022
View reviewed changes
src/algebra/module/projective.lean Outdated Show resolved Hide resolved
src/algebra/module/projective.lean Outdated Show resolved Hide resolved
src/algebra/module/projective.lean Outdated Show resolved Hide resolved
src/linear_algebra/finsupp.lean Outdated Show resolved Hide resolved
@tb65536 tb65536 added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Oct 1, 2022
@antoinelab01 antoinelab01 added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Oct 1, 2022
@fpvandoorn fpvandoorn added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Oct 3, 2022
@bors
Copy link

bors bot commented Oct 3, 2022

✌️ antoinelab01 can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@fpvandoorn
Copy link
Member

But note that there is a merge conflict, so please merge master before running bors merge

@antoinelab01
Copy link
Collaborator Author

bors r+

@bors
Copy link

bors bot commented Oct 5, 2022

👎 Rejected by label

@fpvandoorn fpvandoorn removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Oct 5, 2022
@fpvandoorn
Copy link
Member

bors merge

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Oct 5, 2022
bors bot pushed a commit that referenced this pull request Oct 5, 2022
@antoinelab01
feat(algebra/module/projective): projective modules are closed under …
6c23329 
…product (#16735)
@bors
Copy link

bors bot commented Oct 5, 2022

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Oct 5, 2022
@antoinelab01
feat(algebra/module/projective): projective modules are closed under …
248bafa 
…product (#16735)
@bors
Copy link

bors bot commented Oct 6, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(algebra/module/projective): projective modules are closed under product [Merged by Bors] - feat(algebra/module/projective): projective modules are closed under product Oct 6, 2022
@bors bors bot closed this Oct 6, 2022
@bors bors bot deleted the projective_prod branch October 6, 2022 00:19
bors bot pushed a commit that referenced this pull request Oct 7, 2022
@antoinelab01
feat(algebra/module/projective): projective modules are closed under …
e8f6bc6 
…direct sums (#16743)

I'm unsure what the universe should be for the index type `ι` in algebra/module/projective (`{ι : Type*}` doesn't work). 

- [x] depends on: #16735 



Co-authored-by: antoinelab01 <66086247+antoinelab01@users.noreply.github.com>
bors bot pushed a commit that referenced this pull request Oct 8, 2022
@antoinelab01
feat(algebra/module/projective): projective modules are closed under …
666d878 
…direct sums (#16743)

I'm unsure what the universe should be for the index type `ι` in algebra/module/projective (`{ι : Type*}` doesn't work). 

- [x] depends on: #16735 



Co-authored-by: antoinelab01 <66086247+antoinelab01@users.noreply.github.com>
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Reviewers

@fpvandoorn fpvandoorn fpvandoorn left review comments

@tb65536 tb65536 tb65536 left review comments

Assignees
No one assigned
Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) t-algebra Algebra (groups, rings, fields etc)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@antoinelab01 @fpvandoorn @tb65536