Skip to content

[Merged by Bors] - chore: rename zpow monotonicity lemmas#18956

Closed
YaelDillies wants to merge 2 commits intomasterfrom
zpow_mono
Closed

[Merged by Bors] - chore: rename zpow monotonicity lemmas#18956
YaelDillies wants to merge 2 commits intomasterfrom
zpow_mono

Conversation

@YaelDillies
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies commented Nov 13, 2024

These new names match the ones introduced in the analogous PR #9095

Open in Gitpod

@YaelDillies YaelDillies added t-algebra Algebra (groups, rings, fields, etc) t-order Order theory labels Nov 13, 2024
@github-actions
Copy link
Copy Markdown

github-actions bot commented Nov 13, 2024 •
edited
Loading

PR summary 6e734fff08

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ zpow_le_zpow_iff_left
+ zpow_le_zpow_iff_right
+ zpow_le_zpow_left
+ zpow_le_zpow_right
+ zpow_left_mono
+ zpow_left_strictMono
+ zpow_lt_zpow_iff_left
+ zpow_lt_zpow_iff_right
+ zpow_lt_zpow_left
+ zpow_lt_zpow_right
+ zpow_right_mono

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.

@YaelDillies YaelDillies added the WIP Work in progress label Nov 13, 2024
@YaelDillies
chore: rename zpow monotonicity lemmas
d1571e2 
These new names match the ones introduced in the analogous PR #9095
@YaelDillies
deprecated aliases
6e734ff
@YaelDillies YaelDillies removed the WIP Work in progress label Nov 13, 2024
Ruben-VandeVelde
Ruben-VandeVelde approved these changes Nov 13, 2024
View reviewed changes
Copy link
Copy Markdown
Contributor

@Ruben-VandeVelde Ruben-VandeVelde left a comment

Choose a reason for hiding this comment

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

maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Nov 13, 2024

🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde.

@github-actions github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Nov 13, 2024
@riccardobrasca
Copy link
Copy Markdown
Member

riccardobrasca commented Nov 13, 2024

Thanks!

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Nov 13, 2024
mathlib-bors bot pushed a commit that referenced this pull request Nov 13, 2024
@YaelDillies
chore: rename zpow monotonicity lemmas (#18956)
ed3a10c 
These new names match the ones introduced in the analogous PR #9095
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Nov 13, 2024

This PR was included in a batch that was canceled, it will be automatically retried

mathlib-bors bot pushed a commit that referenced this pull request Nov 13, 2024
@YaelDillies
chore: rename zpow monotonicity lemmas (#18956)
a3376cb 
These new names match the ones introduced in the analogous PR #9095
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Nov 13, 2024

Build failed (retrying...):

mathlib-bors bot pushed a commit that referenced this pull request Nov 13, 2024
@YaelDillies
chore: rename zpow monotonicity lemmas (#18956)
798302c 
These new names match the ones introduced in the analogous PR #9095
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Nov 13, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore: rename zpow monotonicity lemmas [Merged by Bors] - chore: rename zpow monotonicity lemmas Nov 13, 2024
@mathlib-bors mathlib-bors bot closed this Nov 13, 2024
@mathlib-bors mathlib-bors bot deleted the zpow_mono branch November 13, 2024 18:30
TobiasLeichtfried pushed a commit that referenced this pull request Nov 21, 2024
@YaelDillies @TobiasLeichtfried
chore: rename zpow monotonicity lemmas (#18956)
71443ae 
These new names match the ones introduced in the analogous PR #9095
@YaelDillies YaelDillies mentioned this pull request Dec 17, 2025
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@Ruben-VandeVelde Ruben-VandeVelde Ruben-VandeVelde approved these changes

Assignees

No one assigned

Labels

maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. ready-to-merge This PR has been sent to bors. t-algebra Algebra (groups, rings, fields, etc) t-order Order theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@YaelDillies @riccardobrasca @Ruben-VandeVelde