Commit 2025-09-28 15:39 ac0e5e15

View on Github →

chore(LinearAlgebra/TensorProduct/Basic): semi-linearize map and lift (#27288) Semi-linearizing TensorProduct.map. This is important as we can then define star on tensors as: star x := map (starLinearEquiv R) (starLinearEquiv R) x. We can then also define the inner product on tensors.

Estimated changes

modified theorem TensorProduct.ext'
modified theorem TensorProduct.lift.tmul'
modified theorem TensorProduct.lift.tmul
modified theorem TensorProduct.lift.unique
modified def TensorProduct.lift
modified def TensorProduct.liftAux
modified theorem TensorProduct.liftAux_tmul
modified def TensorProduct.map
modified theorem TensorProduct.map_comp
modified theorem TensorProduct.map_map
modified theorem TensorProduct.map_tmul