From eeac62e4648b069297879189e62745b22cbdc6ef Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Thu, 20 Jun 2024 10:37:42 +0200 Subject: [PATCH] remove porting notes --- Mathlib/LinearAlgebra/TensorProduct/Tower.lean | 4 ---- 1 file changed, 4 deletions(-) diff --git a/Mathlib/LinearAlgebra/TensorProduct/Tower.lean b/Mathlib/LinearAlgebra/TensorProduct/Tower.lean index 7d9cbe8864980f..6c6c9e70f419b4 100644 --- a/Mathlib/LinearAlgebra/TensorProduct/Tower.lean +++ b/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}