Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-06 01:49 0cc1fee5

View on Github →

feat(linear_algebra/finsupp): lemmas for finsupp_tensor_finsupp (#6905)

Estimated changes

Modified src/linear_algebra/direct_sum/finsupp.lean

added def finsupp_tensor_finsupp'

added theorem finsupp_tensor_finsupp'_apply_apply

added theorem finsupp_tensor_finsupp'_single_tmul_single

added theorem finsupp_tensor_finsupp_apply

Modified src/linear_algebra/finsupp.lean

added theorem finsupp.lcongr_apply_apply

modified theorem finsupp.lcongr_single

added theorem finsupp.lcongr_symm

added theorem finsupp.lcongr_symm_single