Commit 2024-10-29 23:03 c96009eb

refactor(LinearAlgebra/BilinearForm/TensorProduct): Tensor products of bilinear maps (#14988) Extend the results in Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean from Bilinear Forms to Bilinear Maps Similarly for LinearAlgebra/QuadraticForm/TensorProduct. I had originally intended to extend much more, but was blocked by not being able to extend LinearMap.IsSymm from forms to maps. The existing BilinMap names were actually specific to bilinear forms; these have been renamed to make room for the generalizations. Moves:

• LinearMap.BilinMap.tensorDistrib → LinearMap.BilinForm.tensorDistrib
• LinearMap.BilinMap.tensorDistrib_tmul → LinearMap.BilinForm.tensorDistrib_tmul
• LinearMap.BilinMap.tmul → LinearMap.BilinForm.tmul
• LinearMap.BilinMap.baseChange → LinearMap.BilinForm.baseChange
• LinearMap.BilinMap.baseChange_tmul → LinearMap.BilinForm.baseChange_tmul