Commit 2025-10-30 11:10 1ae76b2a

View on Github →

chore(LinearAlgebra/TensorProduct/Basic): more semi-linearizing (#27353)

Estimated changes

Modified Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean

Modified Mathlib/Algebra/Category/ModuleCat/Monoidal/Closed.lean

Modified Mathlib/Algebra/Lie/TensorProduct.lean

Modified Mathlib/Analysis/InnerProductSpace/TensorProduct.lean

Modified Mathlib/CategoryTheory/Monoidal/Internal/Module.lean

Modified Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean

Modified Mathlib/LinearAlgebra/Coevaluation.lean

Modified Mathlib/LinearAlgebra/Contraction.lean

Modified Mathlib/LinearAlgebra/DirectSum/TensorProduct.lean

Modified Mathlib/LinearAlgebra/Dual/Lemmas.lean

Modified Mathlib/LinearAlgebra/TensorProduct/Basic.lean

modified def TensorProduct.congr

modified theorem TensorProduct.congr_symm

modified theorem TensorProduct.congr_symm_tmul

modified theorem TensorProduct.congr_tmul

modified theorem TensorProduct.congr_trans

modified def TensorProduct.curry

modified theorem TensorProduct.curry_apply

modified theorem TensorProduct.curry_injective

modified theorem TensorProduct.ext

modified theorem TensorProduct.ext_fourfold'

modified theorem TensorProduct.ext_fourfold

modified theorem TensorProduct.ext_threefold'

modified theorem TensorProduct.ext_threefold

modified def TensorProduct.homTensorHomMap

modified theorem TensorProduct.homTensorHomMap_apply

modified def TensorProduct.lTensorHomToHomLTensor

modified theorem TensorProduct.lTensorHomToHomLTensor_apply

modified def TensorProduct.lcurry

modified theorem TensorProduct.lcurry_apply

modified def TensorProduct.lift.equiv

modified theorem TensorProduct.lift.equiv_apply

modified theorem TensorProduct.lift.equiv_symm_apply

modified theorem TensorProduct.lift_comp_comm_eq

modified theorem TensorProduct.lift_comp_map

added theorem TensorProduct.lift_compr₂ₛₗ

added theorem TensorProduct.lift_mk_compr₂ₛₗ

modified def TensorProduct.mapBilinear

modified theorem TensorProduct.mapBilinear_apply

modified theorem TensorProduct.map_add_left

modified theorem TensorProduct.map_add_right

modified theorem TensorProduct.map_comm

modified theorem TensorProduct.map_comp_comm_eq

modified theorem TensorProduct.map_smul_left

modified theorem TensorProduct.map_smul_right

modified theorem TensorProduct.map_zero_left

modified theorem TensorProduct.map_zero_right

modified def TensorProduct.map₂

modified theorem TensorProduct.map₂_apply_tmul

modified def TensorProduct.rTensorHomToHomRTensor

modified theorem TensorProduct.rTensorHomToHomRTensor_apply

modified theorem TensorProduct.toLinearMap_congr

modified def TensorProduct.uncurry

modified theorem TensorProduct.uncurry_apply

Modified Mathlib/LinearAlgebra/Trace.lean

modified theorem LinearMap.trace_tensorProduct

Modified Mathlib/RepresentationTheory/Rep.lean