chore(data/finsupp): move and rename finsupp.single_apply_left (#17357

)

This lemma was known as `basis.finsupp.single_apply_left` and lived in `linear_algebra/basis.lean` but it doesn't have anything to do with a basis, so we rename it to just `finsupp.single_apply_left` and move it to a file with less dependencies.

src/data/finsupp/defs.lean

@@ -214,6 +214,11 @@ end⟩
 lemma single_apply [decidable (a = a')] : single a b a' = if a = a' then b else 0 :=
 by convert rfl
 
+lemma single_apply_left {f : α → β} (hf : function.injective f)
+  (x z : α) (y : M) :
+  single (f x) y (f z) = single x y z :=
+by simp only [single_apply, hf.eq_iff]
+
 lemma single_eq_indicator : ⇑(single a b) = set.indicator {a} (λ _, b) :=
 by { ext, simp [single_apply, set.indicator, @eq_comm _ a] }
 

src/linear_algebra/basis.lean

@@ -361,12 +361,6 @@ else
   by letI : subsingleton R := not_nontrivial_iff_subsingleton.mp h; exact
     basis.of_repr (module.subsingleton_equiv R M (range b))
 
-lemma finsupp.single_apply_left {α β γ : Type*} [has_zero γ]
-  {f : α → β} (hf : function.injective f)
-  (x z : α) (y : γ) :
-  finsupp.single (f x) y (f z) = finsupp.single x y z :=
-by simp [finsupp.single_apply, hf.eq_iff]
-
 lemma reindex_range_self (i : ι) (h := set.mem_range_self i) :
   b.reindex_range ⟨b i, h⟩ = b i :=
 begin

src/linear_algebra/finsupp_vector_space.lean

@@ -108,7 +108,7 @@ begin
   by_cases h : i = j,
   { cases h,
     simp only [basis_repr, single_eq_same, basis.repr_self,
-               basis.finsupp.single_apply_left sigma_mk_injective] },
+               finsupp.single_apply_left sigma_mk_injective] },
   simp only [basis_repr, single_apply, h, false_and, if_false, linear_equiv.map_zero, zero_apply]
 end
 

src/linear_algebra/std_basis.lean

@@ -216,7 +216,7 @@ begin
     simp only [pi.basis, linear_equiv.trans_apply, basis.repr_self, std_basis_same,
         linear_equiv.Pi_congr_right_apply, finsupp.sigma_finsupp_lequiv_pi_finsupp_symm_apply],
     symmetry,
-    exact basis.finsupp.single_apply_left
+    exact finsupp.single_apply_left
       (λ i i' (h : (⟨j, i⟩ : Σ j, ιs j) = ⟨j, i'⟩), eq_of_heq (sigma.mk.inj h).2) _ _ _ },
   simp only [pi.basis, linear_equiv.trans_apply, finsupp.sigma_finsupp_lequiv_pi_finsupp_symm_apply,
       linear_equiv.Pi_congr_right_apply],