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 : add lemma on nilpotent and powers #8831

Closed
wants to merge 6 commits into from
Closed

[Merged by Bors] - feat : add lemma on nilpotent and powers #8831

wants to merge 6 commits into from

Conversation

XavierXarles
Copy link
Collaborator

@XavierXarles XavierXarles commented Dec 5, 2023 •
edited by riccardobrasca

Changed IsNilpotent.pow to IsNilpotent.pow_succ. Added IsNilpotent.of_pow and IsNilpotent.pow_iff_pos.

Open in Gitpod

@riccardobrasca riccardobrasca self-assigned this Dec 6, 2023
riccardobrasca
riccardobrasca approved these changes Dec 6, 2023
View reviewed changes
Copy link
Member

@riccardobrasca riccardobrasca left a comment

Choose a reason for hiding this comment

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

The diff says you deleted the .gitignore file, can you revert that change?

Mathlib/RingTheory/Nilpotent.lean Outdated Show resolved Hide resolved
@XavierXarles @riccardobrasca
Update Mathlib/RingTheory/Nilpotent.lean
ccd1e65 
Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>
@XavierXarles
Copy link
Collaborator Author

The diff says you deleted the .gitignore file, can you revert that change?

The problem is that for some reason the .gitignore file in my computer was different of the .gitignore in mathlib4. I did not want to delete the file, just to revert the changes.

@riccardobrasca
Copy link
Member

I've pushed a commit that fixes it. It should be good now. Thanks!

bors d+

@mathlib-bors
Copy link

mathlib-bors bot commented Dec 6, 2023

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

@XavierXarles
Copy link
Collaborator Author

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

bors r+

mathlib-bors bot pushed a commit that referenced this pull request Dec 6, 2023
@XavierXarles @riccardobrasca
feat : add lemma on nilpotent and powers (#8831)
b911116 
Changed `IsNilpotent.pow to IsNilpotent.pow_succ`. Added `IsNilpotent.of_pow` and `IsNilpotent.pow_iff_pos`.



Co-authored-by: Xavier Xarles <56635243+XavierXarles@users.noreply.github.com>
Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>
@mathlib-bors
Copy link

mathlib-bors bot commented Dec 6, 2023

Build failed (retrying...):

@riccardobrasca
Copy link
Member

bors r-

@mathlib-bors
Copy link

mathlib-bors bot commented Dec 6, 2023

Canceled.

@riccardobrasca
Copy link
Member

There is a build error (due to the fact that the variable is now implicit I guess). Can you fix it please? In general it's a good idea to wait for CI to finish before merging the PR (meaning to wait that all the checks are green).

@riccardobrasca
Copy link
Member

Thanks!

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Dec 6, 2023
mathlib-bors bot pushed a commit that referenced this pull request Dec 6, 2023
@XavierXarles @riccardobrasca
feat : add lemma on nilpotent and powers (#8831)
796fc3f 
Changed `IsNilpotent.pow to IsNilpotent.pow_succ`. Added `IsNilpotent.of_pow` and `IsNilpotent.pow_iff_pos`.



Co-authored-by: Xavier Xarles <56635243+XavierXarles@users.noreply.github.com>
Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>
@mathlib-bors
Copy link

mathlib-bors bot commented Dec 6, 2023

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat : add lemma on nilpotent and powers [Merged by Bors] - feat : add lemma on nilpotent and powers Dec 6, 2023
@mathlib-bors mathlib-bors bot closed this Dec 6, 2023
@mathlib-bors mathlib-bors bot deleted the Nilpotent_pow branch December 6, 2023 22:43
awueth pushed a commit that referenced this pull request Dec 19, 2023
@XavierXarles @riccardobrasca @awueth
feat : add lemma on nilpotent and powers (#8831)
c36fba9 
Changed `IsNilpotent.pow to IsNilpotent.pow_succ`. Added `IsNilpotent.of_pow` and `IsNilpotent.pow_iff_pos`.



Co-authored-by: Xavier Xarles <56635243+XavierXarles@users.noreply.github.com>
Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@riccardobrasca riccardobrasca Awaiting requested review from riccardobrasca

Assignees

@riccardobrasca riccardobrasca

Labels
delegated 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
2 participants
@XavierXarles @riccardobrasca