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.NonZeroDivisors #1717

Closed
wants to merge 8 commits into from
Closed

[Merged by Bors] - feat: port RingTheory.NonZeroDivisors #1717

wants to merge 8 commits into from

Conversation

xroblot
Copy link
Collaborator

@xroblot xroblot commented Jan 20, 2023

Open in Gitpod

@xroblot
feat: port RingTheory.NonZeroDivisors
e82f543
@xroblot
Initial file copy from mathport
6332b7e
@xroblot
automated fixes
f1377c8 
Mathbin -> Mathlib

fix certain import statements

move "by" to end of line

add import to Mathlib.lean
@xroblot xroblot added WIP Work in progress mathlib-port This is a port of a theory file from mathlib. labels Jan 20, 2023
@ericrbg
Copy link
Collaborator

ericrbg commented Jan 20, 2023

ahh, I forgot to open a PR!

@ericrbg
Copy link
Collaborator

ericrbg commented Jan 20, 2023

and I was just gonna push my diverging changes and then you're done as well LOL

@xroblot
Copy link
Collaborator Author

xroblot commented Jan 20, 2023

Well, we can compare our solutions :)

How did you fix the notation not working?

And what about the Multiset.induction not working in the last lemma?

@ericrbg
Copy link
Collaborator

ericrbg commented Jan 20, 2023

The notation did work for me, I just had to open nonZeroDivisors. and the induction I wasn't super happy with, I think you found a better solution but I couldn't seem to get induction with working. Let me push some of these changes in:

@xroblot
Copy link
Collaborator Author

xroblot commented Jan 20, 2023

The notation did work for me, I just had to open nonZeroDivisors. and the induction I wasn't super happy with, I think you found a better solution but I couldn't seem to get induction with working. Let me push some of these changes in:

Yes, please do include your notation fix that is definitely better than mine

@ericrbg ericrbg added WIP Work in progress awaiting-review The author would like community review of the PR and removed WIP Work in progress labels Jan 20, 2023
@ericrbg
Copy link
Collaborator

ericrbg commented Jan 20, 2023

have a look, I don;t think I changed that much and it all seems good

@ericrbg ericrbg removed the WIP Work in progress label Jan 20, 2023
@xroblot
Copy link
Collaborator Author

xroblot commented Jan 20, 2023

Very well. Thanks!

jcommelin
jcommelin reviewed Jan 20, 2023
View reviewed changes
Mathlib/RingTheory/NonZeroDivisors.lean Outdated Show resolved Hide resolved
Mathlib/RingTheory/NonZeroDivisors.lean Outdated Show resolved Hide resolved
@jcommelin
Copy link
Member

LGTM

bors d+

@bors
Copy link

bors bot commented Jan 20, 2023

✌️ xroblot 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 delegated and removed awaiting-review The author would like community review of the PR labels Jan 20, 2023
@xroblot
Copy link
Collaborator Author

xroblot commented Jan 20, 2023

bors r+

@ericrbg @jcommelin
remove notes
f9c816d 
Co-authored-by: Johan Commelin <johan@commelin.net>
@bors
Copy link

bors bot commented Jan 20, 2023

Canceled.

@ericrbg
Copy link
Collaborator

ericrbg commented Jan 20, 2023

try again, sorry we need to remove the notes!

@xroblot
Copy link
Collaborator Author

xroblot commented Jan 20, 2023

bors r+

bors bot pushed a commit that referenced this pull request Jan 20, 2023
@xroblot @ericrbg
feat: port RingTheory.NonZeroDivisors (#1717)
5d81ca1 
Co-authored-by: Eric Rodriguez <37984851+ericrbg@users.noreply.github.com>
@bors
Copy link

bors bot commented Jan 20, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: port RingTheory.NonZeroDivisors [Merged by Bors] - feat: port RingTheory.NonZeroDivisors Jan 20, 2023
@bors bors bot closed this Jan 20, 2023
@bors bors bot deleted the port/RingTheory.NonZeroDivisors branch January 20, 2023 18:26
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@jcommelin jcommelin jcommelin left review comments

Assignees
No one assigned
Labels
delegated mathlib-port This is a port of a theory file from mathlib.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@xroblot @ericrbg @jcommelin