mathlib

53b216bc - refactor(algebra/order/ring): Make `strict_ordered_semiring`s nontrivial (#17394)

refactor(algebra/order/ring): Make `strict_ordered_semiring`s nontrivial (#17394) `strict_ordered_semiring` + `nontrivial` implies `char_zero`, but this can't be instance because `char_zero` implies `nontrivial` Instead of waiting for Lean 4, where such looping instances are possible, we make all `strict_ordered_semiring`s nontrivial, because we don't care about types with one element being`strict_ordered_semiring`s.