Theorem TensorProduct.congr_trans

Modification history

2025-10-31 17:31
Mathlib/LinearAlgebra/TensorProduct/Basic.lean
feat(Algebra/Star/LinearMap): `star mul' = mul' ∘ TensorProduct.comm` and `star (f ⊗ₘ g) = star f ⊗ₘ star g` (#31003)
Modified TensorProduct.congr_transView on Github →
2025-10-30 11:10
Mathlib/LinearAlgebra/TensorProduct/Basic.lean
chore(LinearAlgebra/TensorProduct/Basic): more semi-linearizing (#27353)
Modified TensorProduct.congr_transView on Github →
2024-04-25 15:18
Mathlib/LinearAlgebra/TensorProduct/Basic.lean
feat(LinearAlgebra/TensorProduct/Basic): add `LinearEquiv.(l|r)Tensor` (#11731) …
Added TensorProduct.congr_transView on Github →