mathlib3

df1179db - feat(algebra/order/archimedean): `archimedean_iff_int_lt`, `archimedean_iff_int_le`, `floor_ring.archimedean` (#15909)

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).