Mathlib v3 is deprecated. Go to Mathlib v4

Theorem archimedean_iff_int_lt

Modification history

2022-08-09 17:00

src/algebra/order/archimedean.lean

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

Added archimedean_iff_int_lt View on Github →