chore(algebra/module): generalize char_zero.of_algebra to char_zero.of_module (#10609)

Author: urkud

src/algebra/algebra/basic.lean

@@ -1220,23 +1220,6 @@ lemma algebra_rat_subsingleton {α} [semiring α] :
 
 end rat
 
-namespace char_zero
-
-variables {R : Type*} (S : Type*) [comm_semiring R] [semiring S] [algebra R S]
-
-lemma of_algebra [char_zero S] : char_zero R :=
-⟨begin
-  suffices : function.injective (algebra_map R S ∘ coe),
-  { exact this.of_comp },
-  convert char_zero.cast_injective,
-  ext n,
-  rw [function.comp_app, ← (algebra_map ℕ _).eq_nat_cast, ← ring_hom.comp_apply,
-      ring_hom.eq_nat_cast],
-  all_goals { apply_instance }
-end⟩
-
-end char_zero
-
 namespace algebra
 open module
 

src/algebra/module/basic.lean

@@ -528,12 +528,22 @@ lemma nat.no_zero_smul_divisors : no_zero_smul_divisors ℕ M :=
 
 variables {M}
 
-lemma eq_zero_of_smul_two_eq_zero {v : M} (hv : 2 • v = 0) : v = 0 :=
+lemma eq_zero_of_two_nsmul_eq_zero {v : M} (hv : 2 • v = 0) : v = 0 :=
 by haveI := nat.no_zero_smul_divisors R M;
 exact (smul_eq_zero.mp hv).resolve_left (by norm_num)
 
 end nat
 
+variables (R M)
+
+/-- If `M` is an `R`-module with one and `M` has characteristic zero, then `R` has characteristic
+zero as well. Usually `M` is an `R`-algebra. -/
+lemma char_zero.of_module [has_one M] [char_zero M] : char_zero R :=
+begin
+  refine ⟨λ m n h, @nat.cast_injective M _ _ _ _ _ _⟩,
+  rw [← nsmul_one, ← nsmul_one, nsmul_eq_smul_cast R m (1 : M), nsmul_eq_smul_cast R n (1 : M), h]
+end
+
 end module
 
 section add_comm_group -- `R` can still be a semiring here
@@ -559,8 +569,7 @@ include R
 
 lemma eq_zero_of_eq_neg {v : M} (hv : v = - v) : v = 0 :=
 begin
-  haveI := nat.no_zero_smul_divisors R M,
-  refine eq_zero_of_smul_two_eq_zero R _,
+  refine eq_zero_of_two_nsmul_eq_zero R _,
   rw two_smul,
   exact add_eq_zero_iff_eq_neg.mpr hv
 end

src/number_theory/number_field.lean

@@ -82,7 +82,7 @@ protected noncomputable def equiv (R : Type*) [comm_ring R] [algebra R K]
 
 variables (K)
 
-instance [number_field K] : char_zero (ring_of_integers K) := char_zero.of_algebra K
+instance [number_field K] : char_zero (ring_of_integers K) := char_zero.of_module _ K
 
 instance [number_field K] : is_dedekind_domain (ring_of_integers K) :=
 is_integral_closure.is_dedekind_domain ℤ ℚ K _