Theorem TensorProduct.finsuppRight_tmul_single

Modification history

2026-01-21 06:56
Mathlib/LinearAlgebra/DirectSum/Finsupp.lean
feat(LinearAlgebra): make TensorProduct.finsuppLeft and friends heterobasic (#33469)
Added TensorProduct.finsuppRight_tmul_singleView on Github →