Skip to content

[Merged by Bors] - chore: Split off and golf ulift field instances #2911

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
Closed
wants to merge 9 commits into from
Closed

[Merged by Bors] - chore: Split off and golf ulift field instances #2911

wants to merge 9 commits into from

Conversation

@YaelDillies
Copy link
Collaborator

@YaelDillies YaelDillies commented Mar 15, 2023 •
edited
Loading

@YaelDillies YaelDillies added the mathlib3-pair This PR is a forward-port of a mathlib3 PR or part of one, either under review or recently merged label Mar 15, 2023
@YaelDillies YaelDillies mentioned this pull request Mar 15, 2023
Closed
@fpvandoorn
Copy link
Member

fpvandoorn commented Mar 17, 2023

Thanks!
Please update Mathlib.lean
bors d+

@bors
Copy link

bors bot commented Mar 17, 2023

✌️ YaelDillies 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 Mar 17, 2023
@eric-wieser
Copy link
Member

eric-wieser commented Mar 17, 2023

Was this done without the aid of mathport?

@YaelDillies
Copy link
Collaborator Author

YaelDillies commented Mar 17, 2023

For the ulift stuff, yes. For the nonneg stuff, no.

eric-wieser
eric-wieser reviewed Mar 17, 2023
View reviewed changes
@fpvandoorn
Copy link
Member

fpvandoorn commented Mar 17, 2023

You still forgot a file in Mathlib.lean. Note that the README contains a script to update the file automatically (as long as you don't have untracked Lean files in your repo).

YaelDillies
YaelDillies commented Mar 17, 2023
View reviewed changes
eric-wieser
eric-wieser reviewed Mar 17, 2023
View reviewed changes
Mathlib/Algebra/Group/ULift.lean
#align ulift.has_int_cast ULift.intCast

@[simp, norm_cast]
theorem up_natCast [NatCast α] (n : ℕ) : up (n : α) = n :=
Copy link
Member

@eric-wieser eric-wieser Mar 17, 2023

Choose a reason for hiding this comment

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

Isn't it nat_cast?

Copy link
Member

@eric-wieser eric-wieser Mar 17, 2023

Choose a reason for hiding this comment

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

Guess it depends where your coin flip landed so this is out of scope.

Copy link
Collaborator Author

@YaelDillies YaelDillies Mar 17, 2023

Choose a reason for hiding this comment

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

Yeah...

@eric-wieser
Copy link
Member

eric-wieser commented Mar 17, 2023 •
edited
Loading

This is forward-porting two PRs (also leanprover-community/mathlib3#18596), not one, right? Please don't do that without making it clear in the PR description.

@YaelDillies
Copy link
Collaborator Author

YaelDillies commented Mar 17, 2023

Sorry, my edit to the PR description seems to have been lost in the many tabs I have open.

eric-wieser
eric-wieser reviewed Mar 17, 2023
View reviewed changes
eric-wieser
eric-wieser approved these changes Mar 17, 2023
View reviewed changes
Copy link
Member

@eric-wieser eric-wieser left a comment

Choose a reason for hiding this comment

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

bors merge

Thanks!

@kim-em kim-em added the ready-to-merge This PR has been sent to bors. label Mar 17, 2023
bors bot pushed a commit that referenced this pull request Mar 17, 2023
@YaelDillies @eric-wieser
chore: Split off and golf ulift field instances (#2911)
4bd333b 
Match leanprover-community/mathlib3#18590 and leanprover-community/mathlib3#18596



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@bors
Copy link

bors bot commented Mar 17, 2023

Build failed (retrying...):

  • Build

bors bot pushed a commit that referenced this pull request Mar 17, 2023
@YaelDillies @eric-wieser
chore: Split off and golf ulift field instances (#2911)
5163d8c 
Match leanprover-community/mathlib3#18590 and leanprover-community/mathlib3#18596



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@bors
Copy link

bors bot commented Mar 17, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title chore: Split off and golf ulift field instances [Merged by Bors] - chore: Split off and golf ulift field instances Mar 17, 2023
@bors bors bot closed this Mar 17, 2023
@bors bors bot deleted the split_field_ulift branch March 17, 2023 15:21
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 approved these changes

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). mathlib3-pair This PR is a forward-port of a mathlib3 PR or part of one, either under review or recently merged 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

@YaelDillies @fpvandoorn @eric-wieser @kim-em