Theorem LinearMap.comm_comp_lTensor_comp_comm_eq

Modification history

2026-02-12 09:07
Mathlib/LinearAlgebra/TensorProduct/Basic.lean
refactor(LinearAlgebra/TensorProduct): split large file (#34798) …
Modified LinearMap.comm_comp_lTensor_comp_comm_eqView on Github →
2023-10-05 09:03
Mathlib/LinearAlgebra/TensorProduct.lean
feat: Right exactness of tensor product of modules (#6447)
Added LinearMap.comm_comp_lTensor_comp_comm_eqView on Github →