[Merged by Bors] - feat(RingTheory/TensorProduct/Basic): Lifting linear maps to base change

[erdOne]

---

[github-actions]

PR summary 9516008453

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ liftBaseChangeEquiv
+ liftBaseChangeEquiv_symm_apply
+ liftBaseChange_comp
+ liftBaseChange_one_tmul
+ liftBaseChange_tmul
+ range_liftBaseChange

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

[eric-wieser]

Do you think it makes sense to recover (M →ₗ[R] N) ≃ₗ[A] (A ⊗[R] M →ₗ[A] N) from curryEquiv and the more general result (that I'm hopefully not imagining) that
(A →ₗ[A] M) ≃ₗ[A] M?

Otherwise LGTM, feel free to ping for a quick merge.

[eric-wieser]

bors merge

Thanks!

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style