feat(linear_algebra/basis): `basis.map_equiv_fun` (#11888)
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`.







leanprover-community/mathlib,leanprover-community/mathlib