mathlib

85c08a60 - feat(algebra/order/ring): `linear_ordered_comm_semiring` (#16456)

feat(algebra/order/ring): `linear_ordered_comm_semiring` (#16456) Add `linear_ordered_comm_semiring`, a typeclass that was missing from the algebraic order hierarchy for some reason and which acquired a few possible uses over time.