Skip to content

[Merged by Bors] - feat: negOnePow n = (-1 : ℤ) ^ n#17967

Closed
YaelDillies wants to merge 3 commits intomasterfrom
cast_neg_one_pow
Closed

[Merged by Bors] - feat: negOnePow n = (-1 : ℤ) ^ n#17967
YaelDillies wants to merge 3 commits intomasterfrom
cast_neg_one_pow

Conversation

@YaelDillies
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies commented Oct 20, 2024

and rename Int.coe_negOnePow to Int.cast_negOnePow for disambiguation

Open in Gitpod

@YaelDillies
feat: negOnePow n = (-1 : ℤ) ^ n
b5259d2 
and rename `Int.coe_negOnePow` to `Int.cast_negOnePow` for disambiguation
@YaelDillies YaelDillies added the t-algebra Algebra (groups, rings, fields, etc) label Oct 20, 2024
@YaelDillies YaelDillies mentioned this pull request Oct 20, 2024
Closed
3 tasks
@github-actions
Copy link
Copy Markdown

github-actions bot commented Oct 20, 2024 •
edited
Loading

PR summary 08b2e17fba

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ cast_negOnePow
+ cast_negOnePow_natCast
+ coe_negOnePow_natCast

You can run this locally as follows 
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

b-mehta
b-mehta approved these changes Oct 20, 2024
View reviewed changes
Copy link
Copy Markdown
Contributor

@b-mehta b-mehta left a comment

Choose a reason for hiding this comment

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

bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Oct 20, 2024

✌️ 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.

@ghost ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Oct 20, 2024
YaelDillies and others added 2 commits October 20, 2024 21:28
@YaelDillies
fix
982c4e8
@YaelDillies @b-mehta
tweaks
08b2e17 
Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>
@YaelDillies
Copy link
Copy Markdown
Contributor Author

YaelDillies commented Oct 20, 2024

bors merge

mathlib-bors bot pushed a commit that referenced this pull request Oct 20, 2024
@YaelDillies
feat: negOnePow n = (-1 : ℤ) ^ n (#17967)
1b6c758 
and rename `Int.coe_negOnePow` to `Int.cast_negOnePow` for disambiguation
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Oct 20, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: negOnePow n = (-1 : ℤ) ^ n [Merged by Bors] - feat: negOnePow n = (-1 : ℤ) ^ n Oct 20, 2024
@mathlib-bors mathlib-bors bot closed this Oct 20, 2024
@mathlib-bors mathlib-bors bot deleted the cast_neg_one_pow branch October 20, 2024 21:50
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@b-mehta b-mehta b-mehta approved these changes

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). t-algebra Algebra (groups, rings, fields, etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@YaelDillies @b-mehta