chore(LinearAlgebra/TensorProduct/Tower): remove superfluous porting notes (#13987)

Author: joneugster

Mathlib/LinearAlgebra/TensorProduct/Tower.lean

@@ -150,7 +150,6 @@ def uncurry : (M →ₗ[A] N →ₗ[R] P) →ₗ[B] M ⊗[R] N →ₗ[A] P where
   toFun := lift
   map_add' _ _ := ext fun x y => by simp only [lift_tmul, add_apply]
   map_smul' _ _ := ext fun x y => by simp only [lift_tmul, smul_apply, RingHom.id_apply]
--- Porting note: new `B` argument
 #align tensor_product.algebra_tensor_module.uncurry TensorProduct.AlgebraTensorModule.uncurryₓ
 
 /-- Heterobasic version of `TensorProduct.lcurry`:
@@ -162,7 +161,6 @@ def lcurry : (M ⊗[R] N →ₗ[A] P) →ₗ[B] M →ₗ[A] N →ₗ[R] P where
   toFun := curry
   map_add' _ _ := rfl
   map_smul' _ _ := rfl
--- Porting note: new `B` argument
 #align tensor_product.algebra_tensor_module.lcurry TensorProduct.AlgebraTensorModule.lcurryₓ
 
 /-- Heterobasic version of `TensorProduct.lift.equiv`:
@@ -174,7 +172,6 @@ def lift.equiv : (M →ₗ[A] N →ₗ[R] P) ≃ₗ[B] M ⊗[R] N →ₗ[A] P :=
   LinearEquiv.ofLinear (uncurry R A B M N P) (lcurry R A B M N P)
     (LinearMap.ext fun _ => ext fun x y => lift_tmul _ x y)
     (LinearMap.ext fun f => LinearMap.ext fun x => LinearMap.ext fun y => lift_tmul f x y)
--- Porting note: new `B` argument
 #align tensor_product.algebra_tensor_module.lift.equiv TensorProduct.AlgebraTensorModule.lift.equivₓ
 
 /-- Heterobasic version of `TensorProduct.mk`:
@@ -341,7 +338,6 @@ def assoc : (M ⊗[A] P) ⊗[R] Q ≃ₗ[B] M ⊗[A] (P ⊗[R] Q) :=
     (lift <| uncurry R A B P Q _ ∘ₗ curry (mk R B _ Q))
     (by ext; rfl)
     (by ext; rfl)
--- Porting note: new `B` argument
 #align tensor_product.algebra_tensor_module.assoc TensorProduct.AlgebraTensorModule.assocₓ
 
 variable {M P N Q}