feat(algebra/algebra/basic): relax typeclass assumptions (#14415)

Author: astrainfinita

src/algebra/algebra/basic.lean

@@ -444,37 +444,31 @@ variables {R A : Type*}
 
 open algebra
 
-section ring
-
-variables [comm_ring R]
-
 /-- If `algebra_map R A` is injective and `A` has no zero divisors,
 `R`-multiples in `A` are zero only if one of the factors is zero.
 
 Cannot be an instance because there is no `injective (algebra_map R A)` typeclass.
 -/
 lemma of_algebra_map_injective
-  [semiring A] [algebra R A] [no_zero_divisors A]
+  [comm_semiring R] [semiring A] [algebra R A] [no_zero_divisors A]
   (h : function.injective (algebra_map R A)) : no_zero_smul_divisors R A :=
 ⟨λ c x hcx, (mul_eq_zero.mp ((smul_def c x).symm.trans hcx)).imp_left
-  ((injective_iff_map_eq_zero (algebra_map R A)).mp h _)⟩
+  (map_eq_zero_iff (algebra_map R A) h).mp⟩
 
 variables (R A)
-lemma algebra_map_injective [ring A] [nontrivial A]
+lemma algebra_map_injective [comm_ring R] [ring A] [nontrivial A]
   [algebra R A] [no_zero_smul_divisors R A] :
   function.injective (algebra_map R A) :=
 suffices function.injective (λ (c : R), c • (1 : A)),
 by { convert this, ext, rw [algebra.smul_def, mul_one] },
 smul_left_injective R one_ne_zero
 
 variables {R A}
-lemma iff_algebra_map_injective [ring A] [is_domain A] [algebra R A] :
+lemma iff_algebra_map_injective [comm_ring R] [ring A] [is_domain A] [algebra R A] :
   no_zero_smul_divisors R A ↔ function.injective (algebra_map R A) :=
 ⟨@@no_zero_smul_divisors.algebra_map_injective R A _ _ _ _,
  no_zero_smul_divisors.of_algebra_map_injective⟩
 
-end ring
-
 section field
 
 variables [field R] [semiring A] [algebra R A]