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] - chore(algebra/char_p/basic): weaken assumptions integral_domain --> semiring+ #6753

Closed
wants to merge 3 commits into from
Closed

[Merged by Bors] - chore(algebra/char_p/basic): weaken assumptions integral_domain --> semiring+ #6753

wants to merge 3 commits into from

Conversation

adomani
Copy link
Collaborator

@adomani adomani commented Mar 18, 2021

Taking advantage of the no_zero_divisors typeclass, the assumptions on some of the results can be weakened.

Open in Gitpod

@adomani @eric-wieser
Update src/algebra/char_p/basic.lean
ab2a995 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@adomani
Copy link
Collaborator Author

adomani commented Mar 18, 2021

Thanks, Eric! CI is really slow today...

eric-wieser
eric-wieser reviewed Mar 18, 2021
View reviewed changes
src/algebra/char_p/basic.lean
Comment on lines +340 to +341
| 1, hc := absurd (eq.refl (1 : ℕ)) (@char_ne_one R _ _ (1 : ℕ) hc)
| (m+2), hc := or.inl (@char_is_prime_of_two_le R _ _ (m+2) hc (nat.le_add_left 2 m))
Copy link
Member

Choose a reason for hiding this comment

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

I wonder - can you remove the @s here?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

I will try to see this, but, if I introduced them, it was because I had to. I will see if they can be removed!

eric-wieser
eric-wieser reviewed Mar 18, 2021
View reviewed changes
Copy link
Member

@eric-wieser eric-wieser left a comment •
edited

Choose a reason for hiding this comment

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

Thanks!

bors d+

@bors
Copy link

bors bot commented Mar 18, 2021

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

@bryangingechen bryangingechen added the delegated The PR author may merge after reviewing final suggestions. label Mar 18, 2021
@adomani adomani mentioned this pull request Mar 18, 2021
Closed
adomani
adomani commented Mar 18, 2021
View reviewed changes
Copy link
Collaborator Author

@adomani adomani left a comment

Choose a reason for hiding this comment

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

I was not able to remove the extra @: I introduced them, since Lean was complaining otherwise. I will merge as is! Thanks!

@eric-wieser
Copy link
Member

eric-wieser commented Mar 18, 2021 •
edited

You didn't introduce the @, you only introduced the _ (because you added an argument); I'm asking if you can remove both the @ and the _. But if not, that's fine.

@adomani
Copy link
Collaborator Author

adomani commented Mar 18, 2021

Removing the @ and the appropriate underscores, Lean says that it cannot find the instance char_p R 1. It is somewhat strange, since I then go on and fill it in with the typeclass assumption hc, but Lean acts in mysterious ways...

@adomani
Copy link
Collaborator Author

adomani commented Mar 18, 2021

bors r+

@eric-wieser eric-wieser 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 delegated The PR author may merge after reviewing final suggestions. labels Mar 18, 2021
bors bot pushed a commit that referenced this pull request Mar 18, 2021
@adomani
chore(algebra/char_p/basic): weaken assumptions integral_domain --> s…
aea7dfb 
…emiring+ (#6753)

Taking advantage of the `no_zero_divisors` typeclass, the assumptions on some of the results can be weakened.
@bors
Copy link

bors bot commented Mar 18, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title chore(algebra/char_p/basic): weaken assumptions integral_domain --> semiring+ [Merged by Bors] - chore(algebra/char_p/basic): weaken assumptions integral_domain --> semiring+ Mar 18, 2021
@bors bors bot closed this Mar 18, 2021
@bors bors bot deleted the adomani_weaken_chap_p branch March 18, 2021 23:42
b-mehta pushed a commit that referenced this pull request Apr 2, 2021
@adomani @b-mehta
chore(algebra/char_p/basic): weaken assumptions integral_domain --> s…
97279ed 
…emiring+ (#6753)

Taking advantage of the `no_zero_divisors` typeclass, the assumptions on some of the results can be weakened.
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

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+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@adomani @eric-wieser @bryangingechen