[Merged by Bors] - feat(LinearAlgebra/TensorProduct/Subalgebra): some linear maps induced by multiplication for subalgebras

[acmepjz]

This is the follow-up of the PR #12498. It is used in the definition of linearly disjointness (#9651).

---

[github-actions]

PR summary a408bb210d

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.LinearAlgebra.TensorProduct.Subalgebra	1157

---

Declarations diff

+ comm_trans_lTensorBot
+ comm_trans_rTensorBot
+ finrank_sup_le_of_free
+ lTensorBot
+ lTensorBot_one_tmul
+ lTensorBot_symm_apply
+ lTensorBot_tmul
+ mulMap
+ mulMap'
+ mulMap'_surjective
+ mulMap_bot_left_eq
+ mulMap_bot_right_eq
+ mulMap_comm
+ mulMap_range
+ mulMap_tmul
+ mulMap_toLinearMap
+ rTensorBot
+ rTensorBot_symm_apply
+ rTensorBot_tmul
+ rTensorBot_tmul_one
+ rank_sup_le_of_free
+ val_mulMap'_tmul

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>

[erdOne]

Thanks!
maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by erdOne.

[jcommelin]

Thanks 🎉

bors merge

[mathlib-bors]

Build failed (retrying...):

• Build

[mathlib-bors]

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

[mathlib-bors]

Canceled.

[acmepjz]

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style