Mathlib v3 is deprecated. Go to Mathlib v4

Theorem floor_ring.archimedean

Modification history

2022-10-03 06:36
src/algebra/order/archimedean.lean
feat(analysis/normed/group/add_circle): define the additive circle (#16201)
Deleted floor_ring.archimedeanView on Github →
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 floor_ring.archimedeanView on Github →