Commit 2026-02-12 09:07 4aa0616a

refactor(LinearAlgebra/TensorProduct): split large file (#34798) Split > 1500-line file Mathlib/LinearAlgebra/TensorProduct/Basic.lean into 3 more manageable chunks:

• Defs.lean: definition of M ⊗ N as a quotient of FreeAddMonoid (M × N) (500 lines)
• Basic.lean: universal property of M ⊗ N, lifting bilinear maps M → N → P to linear maps M ⊗ N → P (380 lines)
• Map.lean: linear maps M ⊗ N → M' ⊗ N' induced by maps M → M' and N → N' (and one-sided versions of that) (750 lines)