Theorem TensorProduct.map₂_apply_tmul

Modification history

2025-10-30 11:10

Mathlib/LinearAlgebra/TensorProduct/Basic.lean

chore(LinearAlgebra/TensorProduct/Basic): more semi-linearizing (#27353)

Modified TensorProduct.map₂_apply_tmul View on Github →

2024-02-28 08:33

Mathlib/LinearAlgebra/TensorProduct.lean

feat(LinearAlgebra/TensorProduct): add `TensorProduct.map₂` (#10986)

Added TensorProduct.map₂_apply_tmul View on Github →