mathlib

57c4a74a - feat(algebra/order/floor): Generalize floor lemmas to ordered_semirings

feat(algebra/order/floor): Generalize floor lemmas to ordered_semirings Many of the lemmas about floor semiring do not require a linear ordering. These have been generalized. Notably, there _may_ be some nicer ways of writing these lemmas down, in particular, suggestions for specifying the `nonpos_or_nonneg` assumptions would be most welcome. Requested by @eric-wieser in #12795