chore(Algebra/Bilinear): deprecate duplicated injectivity lemmas (#19231)

These are less general versions of results stated elsewhere.
This partially deprecates @Vierkantor's leanprover-community/mathlib3#6588.

Also tidy the one caller of these lemmas.

Author: eric-wieser

Mathlib/Algebra/Algebra/Bilinear.lean

@@ -225,22 +225,19 @@ section Ring
 
 variable {R A : Type*} [CommSemiring R] [Ring A] [Algebra R A]
 
+@[deprecated mul_right_injective₀ (since := "2024-11-18")]
 theorem mulLeft_injective [NoZeroDivisors A] {x : A} (hx : x ≠ 0) :
-    Function.Injective (mulLeft R x) := by
-  letI : Nontrivial A := ⟨⟨x, 0, hx⟩⟩
-  letI := NoZeroDivisors.to_isDomain A
-  exact mul_right_injective₀ hx
+    Function.Injective (mulLeft R x) :=
+  mul_right_injective₀ hx
 
+@[deprecated mul_left_injective₀ (since := "2024-11-18")]
 theorem mulRight_injective [NoZeroDivisors A] {x : A} (hx : x ≠ 0) :
-    Function.Injective (mulRight R x) := by
-  letI : Nontrivial A := ⟨⟨x, 0, hx⟩⟩
-  letI := NoZeroDivisors.to_isDomain A
-  exact mul_left_injective₀ hx
-
-theorem mul_injective [NoZeroDivisors A] {x : A} (hx : x ≠ 0) : Function.Injective (mul R A x) := by
-  letI : Nontrivial A := ⟨⟨x, 0, hx⟩⟩
-  letI := NoZeroDivisors.to_isDomain A
-  exact mul_right_injective₀ hx
+    Function.Injective (mulRight R x) :=
+  mul_left_injective₀ hx
+
+@[deprecated mul_right_injective₀ (since := "2024-11-18")]
+theorem mul_injective [NoZeroDivisors A] {x : A} (hx : x ≠ 0) : Function.Injective (mul R A x) :=
+   mul_right_injective₀ hx
 
 end Ring
 

Mathlib/RingTheory/Ideal/Basis.lean

@@ -21,7 +21,7 @@ variable {ι R S : Type*} [CommSemiring R] [CommRing S] [IsDomain S] [Algebra R
 noncomputable def basisSpanSingleton (b : Basis ι R S) {x : S} (hx : x ≠ 0) :
     Basis ι R (span ({x} : Set S)) :=
   b.map <|
-    LinearEquiv.ofInjective (Algebra.lmul R S x) (LinearMap.mul_injective hx) ≪≫ₗ
+    LinearEquiv.ofInjective (LinearMap.mulLeft R x) (mul_right_injective₀ hx) ≪≫ₗ
         LinearEquiv.ofEq _ _
           (by
             ext
@@ -33,7 +33,7 @@ theorem basisSpanSingleton_apply (b : Basis ι R S) {x : S} (hx : x ≠ 0) (i :
     (basisSpanSingleton b hx i : S) = x * b i := by
   simp only [basisSpanSingleton, Basis.map_apply, LinearEquiv.trans_apply,
     Submodule.restrictScalarsEquiv_apply, LinearEquiv.ofInjective_apply, LinearEquiv.coe_ofEq_apply,
-    LinearEquiv.restrictScalars_apply, Algebra.coe_lmul_eq_mul, LinearMap.mul_apply']
+    LinearEquiv.restrictScalars_apply, LinearMap.mulLeft_apply, LinearMap.mul_apply']
 
 @[simp]
 theorem constr_basisSpanSingleton {N : Type*} [Semiring N] [Module N S] [SMulCommClass R N S]