Mathlib v3 is deprecated. Go to Mathlib v4

Theorem floor_ring_unique

Modification history

2021-10-27 17:47
src/algebra/order/floor.lean
chore(algebra/order/floor): prove `subsingleton`s (#9996)
Deleted floor_ring_uniqueView on Github →
2019-09-27 07:02
src/algebra/floor.lean
chore(*): drop some unused args reported by `#sanity_check_mathlib` (#1490) …
Modified floor_ring_uniqueView on Github →
2019-09-08 16:37
src/algebra/floor.lean
feat(algebra/floor): Split floor from archimedean file. (#1372) …
Added floor_ring_uniqueView on Github →