Theorem LinearMap.lTensor_comp_comm

Modification history

2026-02-12 09:07
Mathlib/LinearAlgebra/TensorProduct/Basic.lean
refactor(LinearAlgebra/TensorProduct): split large file (#34798) …
Modified LinearMap.lTensor_comp_commView on Github →
2025-12-17 10:18
Mathlib/LinearAlgebra/TensorProduct/Basic.lean
chore(LinearAlgebra/TensorProduct/Basic): some API for `lTensor` and `rTensor` (#32854)
Added LinearMap.lTensor_comp_commView on Github →