Theorem finsuppTensorFinsupp'_single_tmul_single

Modification history

2024-02-25 23:46
Mathlib/LinearAlgebra/DirectSum/Finsupp.lean
chore: generalize more `DirectSum` results to avoid negation (#10965) …
Modified finsuppTensorFinsupp'_single_tmul_singleView on Github →
2023-04-01 22:20
Mathlib/LinearAlgebra/DirectSum/Finsupp.lean
feat: port LinearAlgebra.DirectSum.Finsupp (#3205)
Added finsuppTensorFinsupp'_single_tmul_singleView on Github →