Commit 2022-08-09 17:00 df1179db
View on Github →feat(algebra/order/archimedean): archimedean_iff_int_lt, archimedean_iff_int_le, floor_ring.archimedean (#15909)
Add lemmas archimedean_iff_int_lt and archimedean_iff_int_le,
analogous to existing lemmas for nat and rat. Deduce that a
linear ordered field that is a floor ring is archimedean (it seems we
currently only have the converse direction).