mathlib
b3f4f007 - chore(algebra/order/nonneg/*): Separate `floor_ring` from `field` (#18596)

Commit
2 years ago
chore(algebra/order/nonneg/*): Separate `floor_ring` from `field` (#18596) Move the `archimedean` and `floor_ring` instances out of `algebra.order.nonneg.field` into a new file `algebra.order.nonneg.floor`.
Author
Parents
Loading