Commit 2023-04-01 22:20 196e4a1e

View on Github →

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

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/DirectSum/Finsupp.lean

added def finsuppTensorFinsupp'

added theorem finsuppTensorFinsupp'_apply_apply

added theorem finsuppTensorFinsupp'_single_tmul_single

added def finsuppTensorFinsupp

added theorem finsuppTensorFinsupp_apply

added theorem finsuppTensorFinsupp_single

added theorem finsuppTensorFinsupp_symm_single