Theorem LinearMap.rTensor_comp_comm

Modification history

2026-02-12 09:07

Mathlib/LinearAlgebra/TensorProduct/Basic.lean

refactor(LinearAlgebra/TensorProduct): split large file (#34798) …

Modified LinearMap.rTensor_comp_comm View 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.rTensor_comp_comm View on Github →