Theorem finsuppTensorFinsupp'_apply_apply

Modification history

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