Skip to content

[Merged by Bors] - feat: port RingTheory.ChainOfDivisors#3056

Closed
ChrisHughes24 wants to merge 12 commits intomasterfrom
port/RingTheory.ChainOfDivisors
Closed

[Merged by Bors] - feat: port RingTheory.ChainOfDivisors#3056
ChrisHughes24 wants to merge 12 commits intomasterfrom
port/RingTheory.ChainOfDivisors

Conversation

@ChrisHughes24
Copy link
Copy Markdown
Member

@ChrisHughes24 ChrisHughes24 commented Mar 23, 2023 •
edited by github-actions bot
Loading

@ChrisHughes24 ChrisHughes24 added WIP Work in progress mathlib-port This is a port of a theory file from mathlib. help-wanted The author needs attention to resolve issues blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) and removed WIP Work in progress help-wanted The author needs attention to resolve issues labels Mar 23, 2023
@kim-em kim-em added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 7, 2023
@Ruben-VandeVelde Ruben-VandeVelde force-pushed the port/RingTheory.ChainOfDivisors branch from fa334be to 6bdb1cc Compare April 13, 2023 15:34
@kim-em kim-em removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 13, 2023
kim-em
kim-em reviewed Apr 20, 2023
View reviewed changes
@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Apr 20, 2023

bors d+

@bors
Copy link
Copy Markdown

bors bot commented Apr 20, 2023

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

@github-actions github-actions bot added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Apr 20, 2023
@ChrisHughes24 @kim-em
Update Mathlib/RingTheory/ChainOfDivisors.lean
59afd65 
Co-authored-by: Scott Morrison <scott@tqft.net>
@Parcly-Taxel Parcly-Taxel removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Apr 20, 2023
@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Apr 20, 2023

This PR/issue depends on:

@ChrisHughes24
Copy link
Copy Markdown
Member Author

ChrisHughes24 commented Apr 20, 2023

bors r+

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Apr 20, 2023
bors bot pushed a commit that referenced this pull request Apr 20, 2023
@ChrisHughes24 @Ruben-VandeVelde
feat: port RingTheory.ChainOfDivisors (#3056)
c80a95d 
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
@bors
Copy link
Copy Markdown

bors bot commented Apr 20, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: port RingTheory.ChainOfDivisors [Merged by Bors] - feat: port RingTheory.ChainOfDivisors Apr 20, 2023
@bors bors bot closed this Apr 20, 2023
@bors bors bot deleted the port/RingTheory.ChainOfDivisors branch April 20, 2023 15:22
kbuzzard pushed a commit that referenced this pull request Apr 22, 2023
@ChrisHughes24 @Ruben-VandeVelde @kbuzzard
feat: port RingTheory.ChainOfDivisors (#3056)
0143fcb 
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
kim-em pushed a commit that referenced this pull request May 10, 2023
@ChrisHughes24 @Ruben-VandeVelde
feat: port RingTheory.ChainOfDivisors (#3056)
f4af9a6 
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@kim-em kim-em kim-em left review comments

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). mathlib-port This is a port of a theory file from mathlib. ready-to-merge This PR has been sent to bors.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@ChrisHughes24 @kim-em @Parcly-Taxel @Ruben-VandeVelde