mathlib

3fcd9102 - feat(order/filter/archimedean): Generalize tendsto_coe_nat_at_top_iff to floor_semirings

feat(order/filter/archimedean): Generalize tendsto_coe_nat_at_top_iff to floor_semirings Many of the filter properties of archimedean rings `R` actually only need that `∀ (x : R), ∃ (n : ℕ), x ≤ ↑n`. This is true more generally of floor semirings. We make this generalization.