Mathlib v3 is deprecated. Go to Mathlib v4

Theorem floor_semiring_unique

Modification history

2021-10-27 17:47
src/algebra/order/floor.lean
chore(algebra/order/floor): prove `subsingleton`s (#9996)
Deleted floor_semiring_uniqueView on Github →
2021-10-22 15:58
src/algebra/floor.lean
feat(algebra/floor): Floor semirings (#9592) …
Added floor_semiring_uniqueView on Github →