[Merged by Bors] - refactor(algebra/module): rename smul_injective hx to smul_left_injective M hx

src/algebra/algebra/tower.lean

@@ -319,7 +319,7 @@ variables [add_comm_group M] [module A M] [module R M] [is_scalar_tower R A M]
 
 lemma lsmul_injective [no_zero_smul_divisors A M] {x : A} (hx : x ≠ 0) :
   function.injective (lsmul R M x) :=
-smul_injective hx
+smul_left_injective _ hx
 
 end algebra
 

src/algebra/module/basic.lean

@@ -436,12 +436,18 @@ section add_comm_group -- `R` can still be a semiring here
 
 variables [semiring R] [add_comm_group M] [module R M]
 
-lemma smul_injective [no_zero_smul_divisors R M] {c : R} (hc : c ≠ 0) :
+section smul_injective
+
+variables (M)
+
+lemma smul_left_injective [no_zero_smul_divisors R M] {c : R} (hc : c ≠ 0) :
   function.injective (λ (x : M), c • x) :=
 λ x y h, sub_eq_zero.mp ((smul_eq_zero.mp
   (calc c • (x - y) = c • x - c • y : smul_sub c x y
                 ... = 0 : sub_eq_zero.mpr h)).resolve_left hc)
 
+end smul_injective
+
 section nat
 
 variables (R) [no_zero_smul_divisors R M] [char_zero R]
@@ -461,14 +467,20 @@ end add_comm_group
 
 section module
 
-variables {R} [ring R] [add_comm_group M] [module R M] [no_zero_smul_divisors R M]
+variables [ring R] [add_comm_group M] [module R M] [no_zero_smul_divisors R M]
+
+section smul_injective
+
+variables (R)
 
 lemma smul_right_injective {x : M} (hx : x ≠ 0) :
   function.injective (λ (c : R), c • x) :=
 λ c d h, sub_eq_zero.mp ((smul_eq_zero.mp
   (calc (c - d) • x = c • x - d • x : sub_smul c d x
                 ... = 0 : sub_eq_zero.mpr h)).resolve_right hx)
 
+end smul_injective
+
 section nat
 
 variables [char_zero R]

src/analysis/convex/basic.lean

@@ -160,7 +160,7 @@ set.ext $ λ z, ⟨λ ⟨a, b, ha, hb, hab, hz⟩,
 begin
   split,
   { rintro ⟨a, b, ha, hb, hab, hx⟩,
-    refine smul_injective hb.ne' ((add_right_inj (a • x)).1 _),
+    refine smul_left_injective _ hb.ne' ((add_right_inj (a • x)).1 _),
     rw [hx, ←add_smul, hab, one_smul] },
   rintro rfl,
   simp only [open_segment_same, mem_singleton],

src/linear_algebra/basis.lean

@@ -533,7 +533,7 @@ begin
         map_smul' := λ c y, _ }⟩,
     { rw [finsupp.add_apply, add_smul] },
     { rw [finsupp.smul_apply, smul_assoc] },
-    { refine smul_right_injective nz _,
+    { refine smul_right_injective _ nz _,
       simp only [finsupp.single_eq_same],
       exact (w (f (default ι) • x)).some_spec },
     { simp only [finsupp.single_eq_same],

src/linear_algebra/tensor_product.lean

@@ -202,7 +202,7 @@ variables {R M : Type*} [comm_ring R] [add_comm_group M] [module R M]
 
 lemma lsmul_injective [no_zero_smul_divisors R M] {x : R} (hx : x ≠ 0) :
   function.injective (lsmul R M x) :=
-smul_injective hx
+smul_left_injective _ hx
 
 lemma ker_lsmul [no_zero_smul_divisors R M] {a : R} (ha : a ≠ 0) :
   (linear_map.lsmul R M a).ker = ⊥ :=