Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-19 07:18 85c08a60

View on Github →

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.

Estimated changes