Theorem LinearEquiv.comm_trans_rTensor_trans_comm_eq

Modification history

2024-04-25 15:18
Mathlib/LinearAlgebra/TensorProduct/Basic.lean
feat(LinearAlgebra/TensorProduct/Basic): add `LinearEquiv.(l|r)Tensor` (#11731) …
Added LinearEquiv.comm_trans_rTensor_trans_comm_eqView on Github →