Theorem TensorProduct.lift_mk_compr₂ₛₗ

Modification history

2025-10-30 11:10

Mathlib/LinearAlgebra/TensorProduct/Basic.lean

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

Added TensorProduct.lift_mk_compr₂ₛₗ View on Github →