[Merged by Bors] - chore(LinearAlgebra/TensorProduct/Tower): remove superfluous porting notes

[joneugster]

---

The porting note was introduced in the generalisation from def uncurry : (M →ₗ[R] N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[R] P to def uncurry : (M →ₗ[A] N →ₗ[R] P) →ₗ[B] M ⊗[R] N →ₗ[A] P in #6035 by @eric-wieser.

Actually I'm unsure if there is still a use for these porting notes describing the ₓ in #align. If so, they could be categorised instead...

[github-actions]

PR summary eeac62e464

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>

[grunweg]

I don't see why these porting notes are useful and removing them is fine. I would appreciate a second opinion... so let's
maintainer merge

Thanks for doing all these small clean-ups around porting notes!

[github-actions]

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

[kmill]

I could be wrong, but I believe these notes are not necessary. I'll just go ahead and merge...

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style

[eric-wieser]

The idea was that this note might help someone using mathport to convert their project, but removing it now almost a year later is probably fine.

Generally I'd be inclined to just leave these and remove them alongside the aligns when that happens.