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:Data.Polynomial.RingDivision #3029

Closed
wants to merge 14 commits into from
Closed

[Merged by Bors] - feat port:Data.Polynomial.RingDivision #3029

wants to merge 14 commits into from

Conversation

mattrobball
Copy link
Collaborator

@mattrobball mattrobball commented Mar 22, 2023 •
edited by github-actions bot

@mattrobball
feat: port Data.Polynomial.RingDivision
9301675
@mattrobball
Initial file copy from mathport
ee2d2b8
@mattrobball
automated fixes
a024586 
Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
@mattrobball
Squashed commit of the following:
73e8c72 
commit 7c42679
Author: Matthew Ballard <matt@mrb.email>
Date:   Tue Mar 21 14:05:54 2023 -0400

    fix last instance; lint; align names

commit 0fc2e49
Merge: e32f149 d98a95a
Author: Matthew Ballard <matt@mrb.email>
Date:   Tue Mar 21 09:58:01 2023 -0400

    Merge branch 'master' into port/RingTheory.Localization.FractionRing

commit e32f149
Merge: 08b64c3 05f2f08
Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Date:   Tue Mar 14 16:32:33 2023 +0100

    Merge remote-tracking branch 'origin/master' into port/RingTheory.Localization.FractionRing

commit 08b64c3
Author: Matej Penciak <matej.penciak@gmail.com>
Date:   Sat Mar 11 19:57:51 2023 -0500

    can't synthesize last instance...

commit 1a71262
Author: Matej Penciak <matej.penciak@gmail.com>
Date:   Sat Mar 11 19:41:11 2023 -0500

    one more declaration to go

commit 2c4203d
Merge: 4840b55 2941a89
Author: Matej Penciak <matej.penciak@gmail.com>
Date:   Sat Mar 11 19:26:03 2023 -0500

    Merge remote-tracking branch 'origin/master' into port/RingTheory.Localization.FractionRing

commit 4840b55
Author: Matej Penciak <matej.penciak@gmail.com>
Date:   Thu Mar 9 22:26:08 2023 -0500

    almost done with file

commit 784b455
Author: Matej Penciak <matej.penciak@gmail.com>
Date:   Thu Mar 9 20:36:50 2023 -0500

    more fixes

commit b04a7e4
Author: Matej Penciak <matej.penciak@gmail.com>
Date:   Thu Mar 9 20:17:35 2023 -0500

    Got started on port

commit 97858e8
Author: Matej Penciak <matej.penciak@gmail.com>
Date:   Thu Mar 9 16:32:52 2023 -0500

    automated fixes

    Mathbin -> Mathlib
    fix certain import statements
    move "by" to end of line
    add import to Mathlib.lean

commit f3e12b0
Author: Matej Penciak <matej.penciak@gmail.com>
Date:   Thu Mar 9 16:32:52 2023 -0500

    Initial file copy from mathport

commit a8e3266
Author: Matej Penciak <matej.penciak@gmail.com>
Date:   Thu Mar 9 16:32:52 2023 -0500

    feat: port RingTheory.Localization.FractionRing
@mattrobball
start fixes
b74c8d3
@mattrobball
fix first pass
ee456c3
@mattrobball
fix another pass
fb44d90
@mattrobball mattrobball added mathlib-port This is a port of a theory file from mathlib. WIP Work in progress labels Mar 22, 2023
@semorrison semorrison added the blocked-by-other-PR This PR depends on another PR to Mathlib label Mar 22, 2023
@semorrison semorrison removed the blocked-by-other-PR This PR depends on another PR to Mathlib label Mar 22, 2023
@semorrison
Copy link
Contributor

This PR/issue depends on:

@mattrobball mattrobball added awaiting-review The author would like community review of the PR and removed WIP Work in progress labels Mar 22, 2023
jcommelin
jcommelin reviewed Mar 23, 2023
View reviewed changes
Mathlib/Data/Polynomial/RingDivision.lean Outdated

/- Porting note: I could not find this and Lean didn't do it automatically. Perhaps it belongs
elsewhere. -/
theorem WithBot.some_eq_nat_cast (n : ℕ) : WithBot.some n = (n : WithBot ℕ) := rfl
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is

theorem Nat.cast_withBot (n : ℕ) : Nat.cast n = WithBot.some n :=

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks!

jcommelin
jcommelin reviewed Mar 23, 2023
View reviewed changes
Mathlib/Data/Polynomial/RingDivision.lean Outdated
@@ -355,32 +364,36 @@ section CommRing

variable [CommRing R]

/- Porting note: due to a diamond, introduced
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't understand how this porting note relates to neighbouring lines or the diff with mathport-output.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sorry. I was a little terse here. I have expanded (and corrected) the note

jcommelin
jcommelin approved these changes Mar 23, 2023
View reviewed changes
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks 🎉

bors merge

@semorrison semorrison added ready-to-merge This PR has been sent to bors. and removed awaiting-review The author would like community review of the PR labels Mar 23, 2023
bors bot pushed a commit that referenced this pull request Mar 23, 2023
@mattrobball
feat port:Data.Polynomial.RingDivision (#3029)
667f285
@bors
Copy link

bors bot commented Mar 23, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat port:Data.Polynomial.RingDivision [Merged by Bors] - feat port:Data.Polynomial.RingDivision Mar 23, 2023
@bors bors bot closed this Mar 23, 2023
@bors bors bot deleted the port/Data.Polynomial.RingDivision branch March 23, 2023 14:21
@eric-wieser eric-wieser mentioned this pull request Mar 27, 2023
Closed
bors bot pushed a commit that referenced this pull request Mar 27, 2023
@YaelDillies
chore: strip trailing spaces in Data.Polynomial.RingDivision (#3126)
b306241 
This was introduced in #3029, due to a combination of `mathport` emitting trailing spaces, and the PR author not using an editor that strips them automatically (unlike vscode which does).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@jcommelin jcommelin jcommelin approved these changes

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.

None yet
3 participants
@mattrobball @semorrison @jcommelin