Def finsuppTensorFinsupp'

Modification history

2024-02-25 23:46

Mathlib/LinearAlgebra/DirectSum/Finsupp.lean

chore: generalize more `DirectSum` results to avoid negation (#10965) …

Modified finsuppTensorFinsupp'View on Github →

2023-04-01 22:20

Mathlib/LinearAlgebra/DirectSum/Finsupp.lean

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

Added finsuppTensorFinsupp'View on Github →