mathlib3

ef139383 - feat(ring_theory/tensor_product): the base change of a linear map along an algebra (#4773)

feat(ring_theory/tensor_product): the base change of a linear map along an algebra (#4773) Co-authored-by: kckennylau <kc_kennylau@yahoo.com.hk> Co-authored-by: Kenny Lau <kc_kennylau@yahoo.com.hk> Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Oliver Nash <github@olivernash.org>