mathlib
4efcda94 - Remove dependence on archimedean in continued fractions

Commit

4 years ago

Remove dependence on archimedean in continued fractions

References

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

Author

khwilson

khwilson

Parents

Loading