archimedean): Generalize tendsto_coe_nat_at_top_iff to floor_semirings
#12795

Open

feat(order/filter/archimedean): Generalize tendsto_coe_nat_at_top_iff to floor_semirings #12795

khwilson wants to merge 3 commits into master from generalize_filter_archimedean

feat(order/filter/archimedean): Generalize tendsto_coe_nat_at_top_iff…

3fcd9102

Remove dependence on archimedean in continued fractions

4efcda94

khwilson added awaiting-CI

Fix linting and lemma reference

744de291

github-actions removed awaiting-CI

khwilson added awaiting-review

eric-wieser commented on 2022-03-18

khwilson removed awaiting-review

khwilson added blocked-by-other-PR

leanprover-community-bot-assistant removed blocked-by-other-PR

leanprover-community-bot-assistant added blocked-by-other-PR

ghost removed blocked-by-other-PR

ghost deleted a comment from leanprover-community-bot-assistant on 2022-08-28

kim-em added awaiting-author

kim-em added merge-conflict

kim-em added awaiting-CI

kim-em added too-late

Reviewers

eric-wieser

Assignees

No one assigned

Labels

awaiting-author merge-conflict awaiting-CI too-late

Milestone

No milestone