Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat: Port RingTheory.NonUnitalSubsemiring.Basic #1774

Closed
wants to merge 13 commits into from
Closed

[Merged by Bors] - feat: Port RingTheory.NonUnitalSubsemiring.Basic #1774

wants to merge 13 commits into from

Conversation

0art0
Copy link
Collaborator

@0art0 0art0 commented Jan 23, 2023

Open in Gitpod

@0art0 0art0 added WIP Work in progress mathlib-port This is a port of a theory file from mathlib. labels Jan 23, 2023
@0art0 0art0 changed the title Port/ring theory.non unital subsemiring.basic feat: Port RingTheory.NonUnitalSubsemiring.Basic Jan 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 Feb 21, 2023
@Ruben-VandeVelde Ruben-VandeVelde force-pushed the port/RingTheory.NonUnitalSubsemiring.Basic branch from 7765a88 to 05cf4af Compare April 6, 2023 21:40
@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 6, 2023
@Ruben-VandeVelde Ruben-VandeVelde marked this pull request as ready for review April 13, 2023 09:58
@Ruben-VandeVelde Ruben-VandeVelde added awaiting-review and removed WIP Work in progress labels Apr 13, 2023
@kim-em
Copy link
Contributor

kim-em commented Apr 14, 2023

I restored the @[mono] attributes, which were implemented since this was opened.

@kim-em
Copy link
Contributor

kim-em commented Apr 14, 2023

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Apr 14, 2023
bors bot pushed a commit that referenced this pull request Apr 14, 2023
@Ruben-VandeVelde @0art0 @kim-em
feat: Port RingTheory.NonUnitalSubsemiring.Basic (#1774)
c7c0f54 
Co-authored-by: ART0 <18333981+0Art0@users.noreply.github.com>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
@bors
Copy link

bors bot commented Apr 15, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: Port RingTheory.NonUnitalSubsemiring.Basic [Merged by Bors] - feat: Port RingTheory.NonUnitalSubsemiring.Basic Apr 15, 2023
@bors bors bot closed this Apr 15, 2023
@bors bors bot deleted the port/RingTheory.NonUnitalSubsemiring.Basic branch April 15, 2023 00:49
kim-em added a commit that referenced this pull request May 10, 2023
@Ruben-VandeVelde @0art0 @kim-em
feat: Port RingTheory.NonUnitalSubsemiring.Basic (#1774)
ebb08bc 
Co-authored-by: ART0 <18333981+0Art0@users.noreply.github.com>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@eric-wieser eric-wieser eric-wieser left review comments

@Vierkantor Vierkantor Vierkantor left review comments

Assignees
No one assigned
Labels
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.
5 participants
@0art0 @kim-em @eric-wieser @Vierkantor @Ruben-VandeVelde