Mathlib v3 is deprecated. Go to Mathlib v4

Theorem archimedean_iff_int_le

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_leView on Github →