feat(algebra/char_zero): add char_zero lemma for ordered_semirings (#…

…6038)

Relevant Zulip chat:

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members

src/algebra/char_zero.lean

@@ -48,10 +48,16 @@ theorem char_zero_of_inj_zero {R : Type*} [add_left_cancel_monoid R] [has_one R]
    rw [H k h, add_zero]
  end⟩
 
+/-- Note this is not an instance as `char_zero` implies `nontrivial`,
+and this would risk forming a loop. -/
+lemma ordered_semiring.to_char_zero {R : Type*} [ordered_semiring R] [nontrivial R] :
+  char_zero R :=
+⟨nat.strict_mono_cast.injective⟩
+
 @[priority 100] -- see Note [lower instance priority]
 instance linear_ordered_semiring.to_char_zero {R : Type*}
   [linear_ordered_semiring R] : char_zero R :=
-⟨nat.strict_mono_cast.injective⟩
+ordered_semiring.to_char_zero
 
 namespace nat
 variables {R : Type*} [add_monoid R] [has_one R] [char_zero R]