Theorem finsuppTensorFinsupp_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 View on Github →

2024-02-22 22:58

Mathlib/LinearAlgebra/DirectSum/Finsupp.lean

feat: generalize direct sum results to avoid negation (#10828) …

Modified finsuppTensorFinsupp_single View on Github →

2023-04-01 22:20

Mathlib/LinearAlgebra/DirectSum/Finsupp.lean

feat: port LinearAlgebra.DirectSum.Finsupp (#3205)

Added finsuppTensorFinsupp_single View on Github →