feat(linear_algebra/basis): basis.map_equiv_fun (#11888)

Add a `simp` lemma about the effect of `equiv_fun` for a basis
obtained with `basis.map`.

src/linear_algebra/basis.lean

@@ -744,6 +744,10 @@ by simp [basis.equiv_fun, finsupp.total_apply, finsupp.sum_fintype]
 @[simp]
 lemma basis.equiv_fun_apply (u : M) : b.equiv_fun u = b.repr u := rfl
 
+@[simp] lemma basis.map_equiv_fun (f : M ≃ₗ[R] M') :
+  (b.map f).equiv_fun = f.symm.trans b.equiv_fun :=
+rfl
+
 lemma basis.sum_equiv_fun (u : M) : ∑ i, b.equiv_fun u i • b i = u :=
 begin
   conv_rhs { rw ← b.total_repr u },