feat(LinearAlgebra/FreeModule): add repr_algebraMap (#21642)

Author: mariainesdff

Mathlib/LinearAlgebra/FreeModule/Basic.lean

@@ -207,3 +207,19 @@ instance tensor : Module.Free S (M ⊗[R] N) :=
 end CommSemiring
 
 end Module.Free
+
+namespace Basis
+
+open Finset
+
+variable {S : Type*} [CommRing R] [Ring S] [Algebra R S]
+
+/-- If `B` is a basis of the `R`-algebra `S` such that `B i = 1` for some index `i`, then
+each `r : R` gets represented as `s • B i` as an element of `S`. -/
+theorem repr_algebraMap {ι : Type*} [DecidableEq ι] {B : Basis ι R S} {i : ι} (hBi : B i = 1)
+    (r : R) : B.repr ((algebraMap R S) r) = fun j : ι ↦ if i = j then r else 0 := by
+  ext j
+  rw [Algebra.algebraMap_eq_smul_one, map_smul, ← hBi, Finsupp.smul_apply, B.repr_self_apply]
+  simp
+
+end Basis

Mathlib/LinearAlgebra/LinearIndependent.lean

@@ -958,6 +958,14 @@ protected theorem LinearMap.linearIndependent_iff_of_disjoint (f : M →ₗ[R] M
     LinearIndependent R (f ∘ v) ↔ LinearIndependent R v :=
   f.linearIndependent_iff_of_injOn <| LinearMap.injOn_of_disjoint_ker le_rfl hf_inj
 
+open Finset in
+/-- If `∑ i, f i • v i = ∑ i, g i • v i`, then for all `i`, `f i = g i`. -/
+theorem LinearIndependent.eq_coords_of_eq [Fintype ι] {v : ι → M} (hv : LinearIndependent R v)
+    {f : ι → R} {g : ι → R} (heq : ∑ i, f i • v i = ∑ i, g i • v i) (i : ι) : f i = g i := by
+  rw [← sub_eq_zero, ← sum_sub_distrib] at heq
+  simp_rw [← sub_smul] at heq
+  exact sub_eq_zero.mp ((linearIndependent_iff'.mp hv) univ (fun i ↦ f i - g i) heq i (mem_univ i))
+
 /-- If `v` is a linearly independent family of vectors and the kernel of a linear map `f` is
 disjoint with the submodule spanned by the vectors of `v`, then `f ∘ v` is a linearly independent
 family of vectors. See also `LinearIndependent.map'` for a special case assuming `ker f = ⊥`. -/