Commit 2022-04-12 15:33 c21561a0

View on Github →

feat(algebra/direct_sum): Reindexing direct sums (#13076) Lemmas to reindex direct sums, as well as to rewrite direct sums over an option or sigma type.

Estimated changes

Modified src/algebra/direct_sum/basic.lean

added def direct_sum.equiv_congr_left

added theorem direct_sum.equiv_congr_left_apply

added theorem direct_sum.sigma_curry_apply

added theorem direct_sum.sigma_uncurry_apply

Modified src/algebra/direct_sum/module.lean

added def direct_sum.lequiv_congr_left

added theorem direct_sum.lequiv_congr_left_apply

added theorem direct_sum.sigma_lcurry_apply

added theorem direct_sum.sigma_luncurry_apply

Modified src/data/dfinsupp/basic.lean

added def dfinsupp.comap_domain'[Π

added theorem dfinsupp.comap_domain'_add

added theorem dfinsupp.comap_domain'_apply

added theorem dfinsupp.comap_domain'_smul

added theorem dfinsupp.comap_domain'_zero

added theorem dfinsupp.comap_domain_add

added theorem dfinsupp.comap_domain_apply

added theorem dfinsupp.comap_domain_smul

added theorem dfinsupp.comap_domain_zero

added def dfinsupp.equiv_congr_left

added theorem dfinsupp.equiv_prod_dfinsupp_add

added theorem dfinsupp.equiv_prod_dfinsupp_smul

added def dfinsupp.extend_with

added theorem dfinsupp.extend_with_none

added theorem dfinsupp.extend_with_some

added theorem dfinsupp.sigma_curry_add

added theorem dfinsupp.sigma_curry_apply

added theorem dfinsupp.sigma_curry_smul

added theorem dfinsupp.sigma_curry_zero

added theorem dfinsupp.sigma_uncurry_add

added theorem dfinsupp.sigma_uncurry_apply

added theorem dfinsupp.sigma_uncurry_smul

added theorem dfinsupp.sigma_uncurry_zero