Theorem LinearEquiv.coe_rTensor_symm

Modification history

2026-07-12 11:31
Mathlib/LinearAlgebra/TensorProduct/Map.lean
chore(LinearAlgebra/TensorProduct/Map): add symm_lTensor and symm_rTensor (#41550) …
Modified LinearEquiv.coe_rTensor_symmView on Github →
2026-02-12 09:07
Mathlib/LinearAlgebra/TensorProduct/Basic.lean
refactor(LinearAlgebra/TensorProduct): split large file (#34798) …
Modified LinearEquiv.coe_rTensor_symmView on Github →
2024-04-25 15:18
Mathlib/LinearAlgebra/TensorProduct/Basic.lean
feat(LinearAlgebra/TensorProduct/Basic): add `LinearEquiv.(l|r)Tensor` (#11731) …
Added LinearEquiv.coe_rTensor_symmView on Github →