chore(LinearIndependent): rename linearCombination lemmas (#23045)

Follow the naming convention around unnamespacing and appending `_injective` better.

From Toric

Author: YaelDillies

Mathlib/LinearAlgebra/LinearIndependent/Basic.lean

@@ -250,7 +250,7 @@ theorem LinearIndependent.disjoint_span_image (hv : LinearIndependent R v) {s t
     (hs : Disjoint s t) : Disjoint (Submodule.span R <| v '' s) (Submodule.span R <| v '' t) := by
   simp only [disjoint_def, Finsupp.mem_span_image_iff_linearCombination]
   rintro _ ⟨l₁, hl₁, rfl⟩ ⟨l₂, hl₂, H⟩
-  rw [hv.injective_linearCombination.eq_iff] at H; subst l₂
+  rw [hv.finsuppLinearCombination_injective.eq_iff] at H; subst l₂
   have : l₁ = 0 := Submodule.disjoint_def.mp (Finsupp.disjoint_supported_supported hs) _ hl₁ hl₂
   simp [this]
 

Mathlib/LinearAlgebra/LinearIndependent/Defs.lean

@@ -115,16 +115,31 @@ variable {R v}
 theorem LinearIndepOn.linearIndependent {s : Set ι} (h : LinearIndepOn R v s) :
     LinearIndependent R (fun x : s ↦ v x) := h
 
-theorem linearIndependent_iff_injective_linearCombination :
+theorem linearIndependent_iff_injective_finsuppLinearCombination :
     LinearIndependent R v ↔ Injective (Finsupp.linearCombination R v) := Iff.rfl
 
-alias ⟨LinearIndependent.injective_linearCombination, _⟩ :=
-  linearIndependent_iff_injective_linearCombination
+@[deprecated (since := "2025-03-18")]
+alias linearIndependent_iff_injective_linearCombination :=
+  linearIndependent_iff_injective_finsuppLinearCombination
 
-theorem Fintype.linearIndependent_iff_injective [Fintype ι] :
+alias ⟨LinearIndependent.finsuppLinearCombination_injective, _⟩ :=
+  linearIndependent_iff_injective_finsuppLinearCombination
+
+@[deprecated (since := "2025-03-18")]
+alias LinearIndependent.linearCombination_injective :=
+  LinearIndependent.finsuppLinearCombination_injective
+
+theorem linearIndependent_iff_injective_fintypeLinearCombination [Fintype ι] :
     LinearIndependent R v ↔ Injective (Fintype.linearCombination R v) := by
   simp [← Finsupp.linearCombination_eq_fintype_linearCombination, LinearIndependent]
 
+@[deprecated (since := "2025-03-18")]
+alias Fintype.linearIndependent_iff_injective :=
+  linearIndependent_iff_injective_fintypeLinearCombination
+
+alias ⟨LinearIndependent.fintypeLinearCombination_injective, _⟩ :=
+  linearIndependent_iff_injective_fintypeLinearCombination
+
 theorem LinearIndependent.injective [Nontrivial R] (hv : LinearIndependent R v) : Injective v := by
   simpa [comp_def]
     using Injective.comp hv (Finsupp.single_left_injective one_ne_zero)
@@ -245,7 +260,7 @@ theorem not_linearIndependent_iffₛ :
 
 theorem Fintype.linearIndependent_iffₛ [Fintype ι] :
     LinearIndependent R v ↔ ∀ f g : ι → R, ∑ i, f i • v i = ∑ i, g i • v i → ∀ i, f i = g i := by
-  simp_rw [Fintype.linearIndependent_iff_injective,
+  simp_rw [linearIndependent_iff_injective_fintypeLinearCombination,
     Injective, Fintype.linearCombination_apply, funext_iff]
 
 theorem Fintype.not_linearIndependent_iffₛ [Fintype ι] :
@@ -581,7 +596,7 @@ theorem linearIndependent_iff'' :
 
 theorem linearIndependent_add_smul_iff {c : ι → R} {i : ι} (h₀ : c i = 0) :
     LinearIndependent R (v + (c · • v i)) ↔ LinearIndependent R v := by
-  simp [linearIndependent_iff_injective_linearCombination,
+  simp [linearIndependent_iff_injective_finsuppLinearCombination,
     ← Finsupp.linearCombination_comp_addSingleEquiv i c h₀]
 
 theorem not_linearIndependent_iff :

Mathlib/LinearAlgebra/RootSystem/Finite/g2.lean

@@ -167,7 +167,7 @@ lemma allRoots_eq_map_allCoeffs :
 
 lemma allRoots_nodup : (allRoots P).Nodup := by
   have hli : Injective (Fintype.linearCombination ℤ ![shortRoot P, longRoot P]) := by
-    rw [← Fintype.linearIndependent_iff_injective]
+    rw [← linearIndependent_iff_injective_fintypeLinearCombination]
     exact (linearIndependent_short_long P).restrict_scalars' ℤ
   rw [allRoots_eq_map_allCoeffs, nodup_map_iff hli]
   decide

Mathlib/RingTheory/AlgebraicIndependent/Basic.lean

@@ -65,14 +65,14 @@ theorem algebraMap_injective : Injective (algebraMap R A) := by
       (MvPolynomial.C_injective _ _)
 
 theorem linearIndependent : LinearIndependent R x := by
-  rw [linearIndependent_iff_injective_linearCombination]
+  rw [linearIndependent_iff_injective_finsuppLinearCombination]
   have : Finsupp.linearCombination R x =
       (MvPolynomial.aeval x).toLinearMap.comp (Finsupp.linearCombination R X) := by
     ext
     simp
   rw [this]
   refine (algebraicIndependent_iff_injective_aeval.mp hx).comp ?_
-  rw [← linearIndependent_iff_injective_linearCombination]
+  rw [← linearIndependent_iff_injective_finsuppLinearCombination]
   exact linearIndependent_X _ _
 
 protected theorem injective [Nontrivial R] : Injective x :=