Def finsuppTensorFinsupp
Modification history
2024-04-26 18:08
Mathlib/LinearAlgebra/DirectSum/Finsupp.lean
feat: Generalize `Basis.tensorProduct` to heterobasic version (#11844) …
Added finsuppTensorFinsuppView on Github →2024-04-08 20:05
Mathlib/LinearAlgebra/DirectSum/Finsupp.lean
feat(Mathlib/LinearAlgebra/DirectSum/Finsupp): tensor products of finsupp sums (#11635) …
Deleted finsuppTensorFinsuppView on Github →2024-02-25 23:46
Mathlib/LinearAlgebra/DirectSum/Finsupp.lean
chore: generalize more `DirectSum` results to avoid negation (#10965) …
Added finsuppTensorFinsuppView on Github →