Scalar extension of linear-map spaces

For a finite free source module, extending the scalars of the space of linear maps is the same as taking linear maps between the scalar-extended modules. This file identifies Mathlib's LinearMap.baseChangeHom as that scalar-extension map, so IsBaseChange.equiv supplies the comparison equivalence and IsBaseChange.equiv_tmul evaluates it on pure tensors.

theorem LinearMap.isBaseChange_baseChangeHom (R : Type u_1) (A : Type u_2) (M : Type u_3) (N : Type u_4) [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module.Free R M] [Module.Finite R M] [AddCommMonoid N] [Module R N] : IsBaseChange A (baseChangeHom R A M N)

Linear maps out of a finite free module commute with scalar extension of both modules.