refactor(LinearAlgebra/Basic): R-linear equivalence between spaces of R₁-linear maps

[mans0954]

trafficstars

Loosens the hypothesis of LinearEquiv.arrowCongr to get an R-linear equivalence between spaces of R₁-linear maps.

This is needed for #9334.

---

[mans0954]

!bench

[leanprover-bot]

Here are the benchmark results for commit 70b3b5f55ab9bb0b414aec18ff4257a5aaad716f. There were no significant changes against commit f4da8e56e23fe10cd2184b17803b8db2caa4155e.

[mans0954]

@eric-wieser do you have a moment to review this please? Thanks.

[github-actions[bot]]

Import summary

No significant changes to the import graph

[github-actions[bot]]

PR summary f6820cf50e

Import changes

No significant changes to the import graph

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

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

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

[mans0954]

Closing this PR as it doesn't seem to be of interest.