refactor(LinearAlgebra/BilinearMap): Left composition, bilinear over different rings

[mans0954]

trafficstars

Generalise compl₂ and compl₁₂ for left composition with maps which are linear over different rings in the first and second variable.

Needed for #9334

---

[mans0954]

!bench

[leanprover-bot]

Here are the benchmark results for commit d7460b6e3000c2d477b03bc762ac9d28c9ef70f9. There were no significant changes against commit 91e688bd4a6eded8f4e52afa18f98d9c0f5c9475.

[mans0954]

@eric-wieser do you have a moment to review this PR please? It's quite a small one.

[github-actions[bot]]

Import summary

No significant changes to the import graph

[mathlib-bors[bot]]

:v: mans0954 can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[github-actions[bot]]

PR summary

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]

bors r+

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style