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(ENNReal/Inv): add lemmas about a * a⁻¹ #14423

Closed
wants to merge 2 commits into from
Closed

[Merged by Bors] - feat(ENNReal/Inv): add lemmas about a * a⁻¹ #14423

wants to merge 2 commits into from

Conversation

urkud
Copy link
Member

@urkud urkud commented Jul 4, 2024 •
edited by YaelDillies
Loading

Cherry-picked from #11143
and moved to reuse ENNReal.div_self_le_one.

Co-authored-by: Yaël Dillies [email protected]

Open in Gitpod

@urkud
feat(ENNReal/Inv): add lemmas about a * a⁻¹
7f5f2a6 
Cherry-picked from #11143
and moved to reuse `ENNReal.div_self_le_one`.

Co-Authored-By: @YaelDillies
@github-actions GitHub Actions
Copy link

github-actions bot commented Jul 4, 2024 •
edited
Loading

PR summary a9996731b0

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ div_ne_zero
+ inv_mul_le_one
+ inv_mul_ne_top
+ mul_inv_le_one
+ mul_inv_ne_top

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

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

@urkud urkud added awaiting-review t-analysis Analysis (normed *, calculus) t-algebra Algebra (groups, rings, fields, etc) labels Jul 4, 2024
YaelDillies
YaelDillies reviewed Jul 4, 2024
View reviewed changes
Mathlib/Data/ENNReal/Inv.lean Outdated Show resolved Hide resolved
Mathlib/Data/ENNReal/Inv.lean Outdated Show resolved Hide resolved
@YaelDillies YaelDillies mentioned this pull request Jul 4, 2024
Closed
2 tasks
@YaelDillies
Copy link
Collaborator

maintainer merge

@github-actions GitHub Actions
Copy link

github-actions bot commented Jul 5, 2024

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

@sgouezel
Copy link
Contributor

sgouezel commented Jul 5, 2024

bors r+

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Jul 5, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jul 5, 2024
@urkud @YaelDillies
feat(ENNReal/Inv): add lemmas about a * a⁻¹ (#14423)
d66f005 
Cherry-picked from #11143
and moved to reuse `ENNReal.div_self_le_one`.

Co-authored-by: Yaël Dillies <[email protected]>
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Jul 5, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(ENNReal/Inv): add lemmas about a * a⁻¹ [Merged by Bors] - feat(ENNReal/Inv): add lemmas about a * a⁻¹ Jul 5, 2024
@mathlib-bors mathlib-bors bot closed this Jul 5, 2024
@mathlib-bors mathlib-bors bot deleted the YK-bergelson-ennreal branch July 5, 2024 08:34
@adomani adomani mentioned this pull request Aug 1, 2024
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@YaelDillies YaelDillies YaelDillies left review comments

Assignees
No one assigned
Labels
maintainer-merge ready-to-merge This PR has been sent to bors. t-algebra Algebra (groups, rings, fields, etc) t-analysis Analysis (normed *, calculus)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@urkud @YaelDillies @sgouezel