Skip to content

[Merged by Bors] - feat(Analysis/SpecificLimits/Basic): add lemmas about limits of fractions#16768

Closed
mariainesdff wants to merge 15 commits intomasterfrom
mariainesdff/specific_limits
Closed

[Merged by Bors] - feat(Analysis/SpecificLimits/Basic): add lemmas about limits of fractions#16768
mariainesdff wants to merge 15 commits intomasterfrom
mariainesdff/specific_limits

Conversation

@mariainesdff
Copy link
Copy Markdown
Contributor

@mariainesdff mariainesdff commented Sep 13, 2024

Used in #15373.

Open in Gitpod

@mariainesdff mariainesdff added awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. t-analysis Analysis (normed *, calculus) labels Sep 13, 2024
@github-actions
Copy link
Copy Markdown

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

PR summary 038a2773e5

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ Filter.EventuallyEq.div_mul_cancel
+ Filter.EventuallyEq.div_mul_cancel_atTop
+ Tendsto.den
+ Tendsto.num
+ Tendsto.num_atTop_iff_den_atTop
+ bdd_le_mul_tendsto_zero
+ bdd_le_mul_tendsto_zero'
+ preimage_const_mul_Ioi_or_Iio
+ tendsto_bdd_div_atTop_nhds_zero
+ tendsto_mod_div_atTop_nhds_zero_nat

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.

@mariainesdff mariainesdff mentioned this pull request Sep 13, 2024
Closed
6 tasks
@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Sep 13, 2024
Ruben-VandeVelde
Ruben-VandeVelde reviewed Sep 13, 2024
View reviewed changes
@Ruben-VandeVelde Ruben-VandeVelde added the awaiting-author A reviewer has asked the author a question or requested changes. label Sep 13, 2024
@mariainesdff mariainesdff removed the awaiting-author A reviewer has asked the author a question or requested changes. label Sep 16, 2024
j-loreaux
j-loreaux reviewed Sep 17, 2024
View reviewed changes
@j-loreaux j-loreaux added the awaiting-author A reviewer has asked the author a question or requested changes. label Sep 17, 2024
@mariainesdff mariainesdff removed the awaiting-author A reviewer has asked the author a question or requested changes. label Oct 2, 2024
fpvandoorn
fpvandoorn reviewed Oct 2, 2024
View reviewed changes
@fpvandoorn fpvandoorn added the awaiting-author A reviewer has asked the author a question or requested changes. label Oct 2, 2024
@faenuccio
Copy link
Copy Markdown
Contributor

faenuccio commented Oct 4, 2024

A stupid remark: do you want "quotients" of "fractions" in the PR title?

@mariainesdff mariainesdff removed the awaiting-author A reviewer has asked the author a question or requested changes. label Oct 10, 2024
fpvandoorn
fpvandoorn reviewed Oct 16, 2024
View reviewed changes
@fpvandoorn fpvandoorn added the awaiting-author A reviewer has asked the author a question or requested changes. label Oct 16, 2024
@mariainesdff mariainesdff changed the title feat(Analysis/SpecificLimits/Basic): add lemmas about limits of quotients feat(Analysis/SpecificLimits/Basic): add lemmas about limits of fractions Oct 16, 2024
@mariainesdff mariainesdff removed the awaiting-author A reviewer has asked the author a question or requested changes. label Oct 16, 2024
@fpvandoorn
Copy link
Copy Markdown
Member

fpvandoorn commented Oct 21, 2024

I added a commit with a little bit of cleanup, this looks good now. (I see that many other results in this file are also about just multiplication, but stated for fields, so that is fine for this as well).

bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Oct 21, 2024

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

@github-actions github-actions bot added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Oct 21, 2024
@mariainesdff
Copy link
Copy Markdown
Contributor Author

mariainesdff commented Oct 21, 2024

bors r+

mathlib-bors bot pushed a commit that referenced this pull request Oct 21, 2024
@mariainesdff @fpvandoorn
feat(Analysis/SpecificLimits/Basic): add lemmas about limits of fract…
c3f00b0 
…ions (#16768)

Used in #15373.



Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Oct 21, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(Analysis/SpecificLimits/Basic): add lemmas about limits of fractions [Merged by Bors] - feat(Analysis/SpecificLimits/Basic): add lemmas about limits of fractions Oct 21, 2024
@mathlib-bors mathlib-bors bot closed this Oct 21, 2024
@mathlib-bors mathlib-bors bot deleted the mariainesdff/specific_limits branch October 21, 2024 19:03
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@fpvandoorn fpvandoorn fpvandoorn left review comments

@j-loreaux j-loreaux j-loreaux left review comments

@Ruben-VandeVelde Ruben-VandeVelde Ruben-VandeVelde left review comments

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). t-analysis Analysis (normed *, calculus)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

5 participants

@mariainesdff @faenuccio @fpvandoorn @j-loreaux @Ruben-VandeVelde