chore: add a helper lemma for linearCombination

leanprover-community · Oct 31, 2024 · 3ff330e · 3ff330e
1 parent ecb2a9e
commit 3ff330e
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 12 deletions.
diff --git a/Mathlib/LinearAlgebra/Finsupp.lean b/Mathlib/LinearAlgebra/Finsupp.lean
@@ -636,9 +636,14 @@ theorem linearCombination_zero : linearCombination R (0 : α → M) = 0 :=
 
 variable {α M}
 
+theorem linearCombination_comp_linear (f : M →ₗ[R] M') :
+    linearCombination R (f ∘ v) = f ∘ₗ linearCombination R v := by
+  ext
+  simp [linearCombination_apply]
+
 theorem apply_linearCombination (f : M →ₗ[R] M') (v) (l : α →₀ R) :
-    f (linearCombination R v l) = linearCombination R (f ∘ v) l := by
-  apply Finsupp.induction_linear l <;> simp (config := { contextual := true })
+    f (linearCombination R v l) = linearCombination R (f ∘ v) l :=
+  congr($(linearCombination_comp_linear R f) l).symm
 
 @[deprecated (since := "2024-08-29")] alias apply_total := apply_linearCombination
 
@@ -1225,10 +1230,8 @@ protected theorem Submodule.finsupp_sum_mem {ι β : Type*} [Zero β] (S : Submo
   AddSubmonoidClass.finsupp_sum_mem S f g h
 
 theorem LinearMap.map_finsupp_linearCombination (f : M →ₗ[R] N) {ι : Type*} {g : ι → M}
-    (l : ι →₀ R) : f (linearCombination R g l) = linearCombination R (f ∘ g) l := by
-  -- Porting note: `(· ∘ ·)` is required.
-  simp only [linearCombination_apply, linearCombination_apply, Finsupp.sum, map_sum, map_smul,
-             (· ∘ ·)]
+    (l : ι →₀ R) : f (linearCombination R g l) = linearCombination R (f ∘ g) l :=
+  apply_linearCombination _ _ _ _
 
 @[deprecated (since := "2024-08-29")] alias LinearMap.map_finsupp_total :=
   LinearMap.map_finsupp_linearCombination

diff --git a/Mathlib/LinearAlgebra/LinearIndependent.lean b/Mathlib/LinearAlgebra/LinearIndependent.lean
@@ -282,18 +282,14 @@ theorem LinearIndependent.map (hv : LinearIndependent R v) {f : M →ₗ[R] M'}
       at hf_inj
   rw [linearIndependent_iff_ker] at hv ⊢
   rw [hv, le_bot_iff] at hf_inj
-  haveI : Inhabited M := ⟨0⟩
-  rw [Finsupp.linearCombination_comp, Finsupp.lmapDomain_linearCombination _ _ f,
-      LinearMap.ker_comp, hf_inj]
-  exact fun _ => rfl
+  rw [Finsupp.linearCombination_comp_linear, LinearMap.ker_comp, hf_inj]
 
 /-- If `v` is an injective family of vectors such that `f ∘ v` is linearly independent, then `v`
     spans a submodule disjoint from the kernel of `f` -/
 theorem Submodule.range_ker_disjoint {f : M →ₗ[R] M'}
     (hv : LinearIndependent R (f ∘ v)) :
     Disjoint (span R (range v)) (LinearMap.ker f) := by
-  rw [linearIndependent_iff_ker, Finsupp.linearCombination_comp,
-      Finsupp.lmapDomain_linearCombination R _ f (fun _ ↦ rfl), LinearMap.ker_comp] at hv
+  rw [linearIndependent_iff_ker, Finsupp.linearCombination_comp_linear, LinearMap.ker_comp] at hv
   rw [disjoint_iff_inf_le, ← Set.image_univ, Finsupp.span_image_eq_map_linearCombination,
     map_inf_eq_map_inf_comap, hv, inf_bot_eq, map_bot]