feat(algebra/char_p): add lemma ring_char_ne_one (#2595)

This lemma is more useful than the extant `false_of_nonzero_of_char_one`
when we are working with the function `ring_char` rather than the `char_p`
Prop.

src/algebra/char_p.lean

@@ -235,6 +235,9 @@ end prio
 lemma false_of_nonzero_of_char_one [nonzero_comm_ring R] [char_p R 1] : false :=
 zero_ne_one $ show (0:R) = 1, from subsingleton.elim 0 1
 
+lemma ring_char_ne_one [nonzero_semiring R] : ring_char R ≠ 1 :=
+by { intros h, apply @zero_ne_one R, symmetry, rw [←nat.cast_one, ring_char.spec, h], }
+
 end char_one
 
 end char_p

src/algebra/ring.lean

@@ -485,6 +485,9 @@ end ring_hom
 
 section prio
 set_option default_priority 100 -- see Note [default priority]
+/-- Predicate for semirings in which zero does not equal one. -/
+class nonzero_semiring (α : Type*) extends semiring α, zero_ne_one_class α
+
 /-- Predicate for commutative semirings in which zero does not equal one. -/
 class nonzero_comm_semiring (α : Type*) extends comm_semiring α, zero_ne_one_class α
 
@@ -501,6 +504,12 @@ lemma succ_ne_self [nonzero_comm_ring α] (a : α) : a + 1 ≠ a :=
 lemma pred_ne_self [nonzero_comm_ring α] (a : α) : a - 1 ≠ a :=
 λ h, one_ne_zero (neg_inj ((add_left_inj a).mp (by { convert h, simp })))
 
+/-- A nonzero commutative semiring is a nonzero semiring. -/
+@[priority 100] -- see Note [lower instance priority]
+instance nonzero_comm_semiring.to_nonzero_semiring {α : Type*} [ncs : nonzero_comm_semiring α] :
+  nonzero_semiring α :=
+{..ncs}
+
 /-- A nonzero commutative ring is a nonzero commutative semiring. -/
 @[priority 100] -- see Note [lower instance priority]
 instance nonzero_comm_ring.to_nonzero_comm_semiring {α : Type*} [I : nonzero_comm_ring α] :