Skip to content

[Merged by Bors] - feat: variant of the binary AM-GM inequality#17877

Closed
FordUniver wants to merge 7 commits intomasterfrom
feat-four_mul_le_add_sq
Closed

[Merged by Bors] - feat: variant of the binary AM-GM inequality#17877
FordUniver wants to merge 7 commits intomasterfrom
feat-four_mul_le_add_sq

Conversation

@FordUniver
Copy link
Copy Markdown
Collaborator

@FordUniver FordUniver commented Oct 17, 2024 •
edited by vihdzp
Loading

added variant of binary AM-GM inequality

Open in Gitpod

@github-actions github-actions bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Oct 17, 2024
@github-actions
Copy link
Copy Markdown

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

PR summary 233eabeabb

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ four_mul_le_pow_two_add
+ four_mul_le_sq_add
+ two_add_two_eq_four

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 reviewed Oct 18, 2024
View reviewed changes
YaelDillies
YaelDillies reviewed Oct 18, 2024
View reviewed changes
YaelDillies
YaelDillies approved these changes Oct 18, 2024
View reviewed changes
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies 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 Oct 18, 2024

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

@github-actions github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Oct 18, 2024
@YaelDillies YaelDillies changed the title Feat: variant of binary AM-GM inequality feat: variant of the binary AM-GM inequality Oct 18, 2024
@FordUniver FordUniver force-pushed the feat-four_mul_le_add_sq branch from fac0a69 to 03331be Compare October 18, 2024 16:44
b-mehta
b-mehta reviewed Oct 18, 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.

Thanks!

bors merge

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Oct 18, 2024
mathlib-bors bot pushed a commit that referenced this pull request Oct 18, 2024
@FordUniver
feat: variant of the binary AM-GM inequality (#17877)
7d20fac 
added variant of binary AM-GM inequality



Co-authored-by: FordUniver <61389961+FordUniver@users.noreply.github.com>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Oct 18, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: variant of the binary AM-GM inequality [Merged by Bors] - feat: variant of the binary AM-GM inequality Oct 18, 2024
@mathlib-bors mathlib-bors bot closed this Oct 18, 2024
@mathlib-bors mathlib-bors bot deleted the feat-four_mul_le_add_sq branch October 18, 2024 19:43
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 left review comments

@YaelDillies YaelDillies YaelDillies approved these changes

Assignees

No one assigned

Labels

maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! 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.

3 participants

@FordUniver @YaelDillies @b-mehta