chore(algebra/module): Swap the naming of `smul_(left|right)_injectiv…

…e` to match the naming guide (#8659)

The naming conventions say:

> An injectivity lemma that uses "left" or "right" should refer to the argument that "changes". For example, a lemma with the statement `a - b = a - c ↔ b = c` could be called `sub_right_inj`.

This corrects the name of `function.injective (λ c : R, c • x)` to be `smul_left_injective` instead of the previous `smul_right_injective`, and vice versa for `function.injective (λ x : M, r • x)`.

This also brings it in line with `mul_left_injective` and `mul_right_injective`.

src/algebra/algebra/tower.lean

@@ -311,7 +311,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_left_injective _ hx
+smul_right_injective _ hx
 
 end algebra
 

src/algebra/module/basic.lean

@@ -457,7 +457,7 @@ section smul_injective
 
 variables (M)
 
-lemma smul_left_injective [no_zero_smul_divisors R M] {c : R} (hc : c ≠ 0) :
+lemma smul_right_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
@@ -490,7 +490,7 @@ section smul_injective
 
 variables (R)
 
-lemma smul_right_injective {x : M} (hx : x ≠ 0) :
+lemma smul_left_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

src/analysis/calculus/fderiv_symmetric.lean

@@ -321,7 +321,7 @@ begin
     simp only [continuous_linear_map.map_add, continuous_linear_map.map_smul, add_right_inj,
       continuous_linear_map.add_apply, pi.smul_apply, continuous_linear_map.coe_smul', add_zero,
       continuous_linear_map.zero_apply, smul_zero, continuous_linear_map.map_zero] at this,
-    exact smul_left_injective F (tpos m).ne' this },
+    exact smul_right_injective F (tpos m).ne' this },
   -- applying `second_derivative_within_at_symmetric_of_mem_interior` to the vectors `z + (t v) v`
   -- and `z + (t w) w`, we deduce that `f'' v w = f'' w v`. Cross terms involving `z` can be
   -- eliminated thanks to the fact proved above that `f'' m z = f'' z m`.
@@ -332,7 +332,7 @@ begin
   rw ← sub_eq_zero at this,
   abel at this,
   simp only [one_gsmul, neg_smul, sub_eq_zero, mul_comm, ← sub_eq_add_neg] at this,
-  apply smul_left_injective F _ this,
+  apply smul_right_injective F _ this,
   simp [(tpos v).ne', (tpos w).ne']
 end
 

src/analysis/convex/basic.lean

@@ -164,7 +164,7 @@ set.ext $ λ z, ⟨λ ⟨a, b, ha, hb, hab, hz⟩,
 begin
   split,
   { rintro ⟨a, b, ha, hb, hab, hx⟩,
-    refine smul_left_injective _ hb.ne' ((add_right_inj (a • x)).1 _),
+    refine smul_right_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/analysis/normed_space/conformal_linear_map.lean

@@ -113,7 +113,7 @@ end
 
 lemma injective {f' : M →L[R] N} (h : is_conformal_map f') : function.injective f' :=
 let ⟨c, hc, li, hf'⟩ := h in by simp only [hf', pi.smul_def];
-  exact (smul_left_injective _ hc).comp li.injective
+  exact (smul_right_injective _ hc).comp li.injective
 
 lemma ne_zero [nontrivial M] {f' : M →L[R] N} (hf' : is_conformal_map f') :
   f' ≠ 0 :=

src/group_theory/complement.lean

@@ -271,11 +271,10 @@ quotient.induction_on α (quotient.induction_on β
       change pow_coprime hH ((pow_coprime hH).symm (diff α β)⁻¹) * (diff α β) = 1,
       rw [equiv.apply_symm_apply, inv_mul_self] }⟩))
 
-lemma smul_injective [H.normal] (α : H.quotient_diff)
-  (hH : nat.coprime (fintype.card H) (fintype.card (quotient_group.quotient H)))
-  {h₁ h₂ : H} (hh : h₁ • α = h₂ • α) : h₁ = h₂ :=
-begin
-  revert hh,
+lemma smul_left_injective [H.normal] (α : H.quotient_diff)
+  (hH : nat.coprime (fintype.card H) (fintype.card (quotient_group.quotient H))) :
+  function.injective (λ h : H, h • α) :=
+λ h₁ h₂, begin
   refine quotient.induction_on α (λ α hα, _),
   replace hα : diff (h₁ • α) (h₂ • α) = 1 := quotient.exact hα,
   rw [smul_diff, ←diff_inv, smul_diff, diff_self, mul_one, mul_inv_eq_one] at hα,
@@ -288,7 +287,7 @@ lemma is_complement_stabilizer_of_coprime [fintype G] [H.normal] {α : H.quotien
 begin
   classical,
   let ϕ : H ≃ mul_action.orbit G α := equiv.of_bijective (λ h, ⟨h • α, h, rfl⟩)
-    ⟨λ h₁ h₂ hh, smul_injective α hH (subtype.ext_iff.mp hh),
+    ⟨λ h₁ h₂ hh, smul_left_injective α hH (subtype.ext_iff.mp hh),
       λ β, exists_imp_exists (λ h hh, subtype.ext hh) (exists_smul_eq α β hH)⟩,
   have key := card_eq_card_quotient_mul_card_subgroup (mul_action.stabilizer G α),
   rw ← fintype.card_congr (ϕ.trans (mul_action.orbit_equiv_quotient_stabilizer G α)) at key,

src/linear_algebra/basis.lean

@@ -591,7 +591,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_left_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_left_injective _ hx
+smul_right_injective _ hx
 
 lemma ker_lsmul [no_zero_smul_divisors R M] {a : R} (ha : a ≠ 0) :
   (linear_map.lsmul R M a).ker = ⊥ :=