chore(algebra/char_p/{basic + algebra}): weaken assumptions for char_…

…p_to_char_zero (#13214)

The assumptions for lemma `char_p_to_char_zero` can be weakened, without changing the proof.

Since the weakening breaks up one typeclass assumption into two, when the lemma was applied with `@`, I inserted an extra `_`.  This happens twice: once in the file where the lemma is, and once in a separate file.

src/algebra/char_p/algebra.lean

@@ -89,7 +89,7 @@ char_p_of_injective_algebra_map (is_fraction_ring.injective R K) p
 
 /-- If `R` has characteristic `0`, then so does Frac(R). -/
 lemma char_zero_of_is_fraction_ring [char_zero R] : char_zero K :=
-@char_p.char_p_to_char_zero K _ (char_p_of_is_fraction_ring R 0)
+@char_p.char_p_to_char_zero K _ _ (char_p_of_is_fraction_ring R 0)
 
 variables [is_domain R]
 

src/algebra/char_p/basic.lean

@@ -328,17 +328,18 @@ namespace char_p
 section
 variables [ring R]
 
-lemma char_p_to_char_zero [char_p R 0] : char_zero R :=
+lemma char_p_to_char_zero (R : Type*) [add_left_cancel_monoid R] [has_one R] [char_p R 0] :
+  char_zero R :=
 char_zero_of_inj_zero $
   λ n h0, eq_zero_of_zero_dvd ((cast_eq_zero_iff R 0 n).mp h0)
 
 lemma cast_eq_mod (p : ℕ) [char_p R p] (k : ℕ) : (k : R) = (k % p : ℕ) :=
 calc (k : R) = ↑(k % p + p * (k / p)) : by rw [nat.mod_add_div]
-         ... = ↑(k % p)               : by simp[cast_eq_zero]
+         ... = ↑(k % p)               : by simp [cast_eq_zero]
 
 theorem char_ne_zero_of_fintype (p : ℕ) [hc : char_p R p] [fintype R] : p ≠ 0 :=
 assume h : p = 0,
-have char_zero R := @char_p_to_char_zero R _ (h ▸ hc),
+have char_zero R := @char_p_to_char_zero R _ _ (h ▸ hc),
 absurd (@nat.cast_injective R _ _ this) (not_injective_infinite_fintype coe)
 
 end