Theorem TensorProduct.map_comp

Modification history

2026-02-12 09:07
Mathlib/LinearAlgebra/TensorProduct/Basic.lean
refactor(LinearAlgebra/TensorProduct): split large file (#34798) …
Modified TensorProduct.map_compView on Github →
2025-09-28 15:39
Mathlib/LinearAlgebra/TensorProduct/Basic.lean
chore(LinearAlgebra/TensorProduct/Basic): semi-linearize `map` and `lift` (#27288) …
Modified TensorProduct.map_compView on Github →
2025-07-25 10:25
Mathlib/LinearAlgebra/TensorProduct/Basic.lean
feat(LinearAlgebra/TensorProduct): `map f₂ g₂ (map f₁ g₁ x) = map (f₂ ∘ₗ f₁) (g₂ ∘ₗ g₁) x` (#27142) …
Modified TensorProduct.map_compView on Github →
2023-03-01 07:31
Mathlib/LinearAlgebra/TensorProduct.lean
feat: port LinearAlgebra.TensorProduct (#2539) …
Added TensorProduct.map_compView on Github →