DFinsupp 📖 | CompData | 564 mathmath: DFinsupp.coprodMap_apply, DirectSum.IsInternal.ofBijective_coeLinearMap_same, DFinsupp.comul_single, DFinsupp.infinite_of_right, Module.Flat.dfinsupp, DFinsupp.liftAddHom_apply, Finsupp.toDFinsupp_add, iSupIndep.linearEquiv_symm_apply, iSupIndep.dfinsupp_lsum_injective, DFinsupp.single_eq_same, DFinsupp.lsum_lsingle, DFinsupp.toMultiset_sup, DirectSum.bracket_apply, DFinsupp.linearIndependent_single_iff, DirectSum.finite_support, sigmaFinsuppEquivDFinsupp_support, DFinsupp.lsingle_apply, MultilinearMap.fromDFinsuppEquiv_apply, DFinsupp.filter_apply_neg, DFinsupp.instIsOrderedCancelAddMonoid, DFinsupp.lex_lt_iff_of_unique, MultilinearMap.dfinsuppFamily_single, DFinsupp.piecewise_single_erase, DirectSum.decompose_of_mem_same, DFinsupp.range_mapRangeAddMonoidHom, Finset.mem_dfinsupp_iff_of_support_subset, Multiset.equivDFinsupp_symm_apply, DFinsupp.liftAddHom_apply_single, Multiset.toDFinsupp_support, DFinsupp.equivFunOnFintype_symm_coe, DFinsupp.mapRange_def, DFinsupp.Lex.acc_zero, DFinsupp.equivProdDFinsupp_smul, DFinsupp.comapDomain'_zero, Pi.comul_comp_dFinsuppCoeFnLinearMap, DFinsupp.zero_apply, Pi.counit_coe_dFinsupp, DFinsupp.extendWith_zero, DirectSum.lie_module_bracket_apply, DFinsupp.sigmaUncurry_add, AddMonoidHom.map_dfinsuppSumAddHom, DFinsupp.prod_add_index, DFinsupp.subtypeDomainLinearMap_apply, DFinsupp.mapRange.linearEquiv_refl, DirectSum.sub_apply, DFinsupp.Lex.wellFounded, sigmaFinsuppAddEquivDFinsupp_apply, iSupIndep.dfinsuppSumAddHom_injective, DFinsupp.disjoint_iff, DFinsupp.neLocus_neg_neg, DFinsupp.coe_mono, DFinsupp.tsub_apply, DFinsupp.sigmaUncurry_single, DFinsupp.sum_zero_index, DFinsupp.toFinsupp_add, DFinsupp.Colex.isOrderedCancelAddMonoid, DFinsupp.equivFunOnFintype_single, DFinsupp.mapRange.linearMap_comp, DFinsupp.toLex_monotone, DFinsupp.update_eq_erase_add_single, DFinsupp.prod_eq_zero_iff, Multiset.Icc_eq, DirectSum.lequivCongrLeft_apply, DFinsupp.mk_neg, DirectSum.lmap_apply, DFinsupp.mapRange.linearEquiv_trans, LinearMap.IsSymmetric.directSum_decompose_apply, DFinsupp.neLocus_self_sub_left, DFinsupp.sumAddHom_single, DFinsupp.subtypeSupportEqEquiv_apply_coe, DFinsupp.coeFnAddMonoidHom_apply, DFinsupp.equivFunOnFintype_apply, DFinsupp.smul_apply, DFinsupp.erase_zero, DirectSum.decompose_eq_mul_idempotent, DFinsupp.Colex.wellFoundedLT, DFinsupp.mapRange.linearEquiv_symm, Multiset.toDFinsupp_apply, DFinsupp.lt_def, Submodule.biSup_eq_range_dfinsupp_lsum, DFinsupp.Lex.isOrderedCancelAddMonoid, DirectSum.coe_of_mul_apply_aux, DFinsupp.subtypeDomain_def, DFinsupp.Colex.addRightMono, DFinsupp.notMem_support_iff, sigmaFinsuppAddEquivDFinsupp_symm_apply, DFinsupp.instSMulPosMono, DFinsupp.equivProdDFinsupp_apply, MultilinearMap.dfinsuppFamily_apply_toFun, MultilinearMap.dfinsuppFamily_apply_support', DirectSum.sum_univ_of, DFinsupp.zipWith_def, DFinsupp.Lex.isOrderedAddMonoid, DFinsupp.smulCommClass, DFinsupp.injective_pi_lapply, DFinsupp.le_iff', DFinsupp.range_mapRangeLinearMap, DFinsupp.coe_tsub, Pi.counit_comp_dFinsuppCoeFnLinearMap, MvPolynomial.weightedDecomposition.decompose'_apply, DFinsupp.mapRange.addMonoidHom_comp, DFinsupp.update_eq_single_add_erase, Finset.card_dfinsupp, AddMonoidHom.coe_dfinsuppSumAddHom, Multiset.equivDFinsupp_apply, DFinsupp.coe_mk', DFinsupp.sum_sum_index, qExpansion_of_mul, DFinsupp.toMultiset_single, DFinsupp.neLocus_self_add_right, DFinsupp.toFinsupp_sub, AdicCompletion.sumInv_apply, DFinsupp.lex_lt_iff, DirectSum.coe_of_mul_apply_add, DFinsupp.mapRange.addEquiv_apply, DFinsupp.sigmaCurry_single, DFinsupp.sigmaCurryLEquiv_apply, DFinsupp.lex_def, sigmaFinsuppEquivDFinsupp_add, DFinsupp.sumZeroHom_apply, DirectSum.coe_decompose_mul_add_of_left_mem, DFinsupp.subtypeDomain_add, AddEquiv.map_dfinsuppSumAddHom, DFinsupp.instIsCocomm, DFinsupp.mem_singleton_apply_iff, DFinsupp.erase_same, DFinsupp.sum_eq_sum_fintype, DFinsupp.coe_sup, DFinsupp.update_eq_sub_add_single, DFinsupp.toFinsupp_smul, Pi.lex_eq_dfinsupp_lex, DFinsupp.single_le_iff, MultilinearMap.dfinsuppFamily_compLinearMap_lsingle, DFinsupp.sum_mapRange_index.linearMap, DFinsupp.mapRange_smul, DFinsupp.prod_sum_index, DirectSum.addEquivProdDirectSum_symm_apply_toFun, MultilinearMap.dfinsuppFamily_add, DFinsupp.prod_eq_prod_fintype, DirectSum.sigmaLcurry_apply, DFinsupp.filter_def, DFinsupp.eraseAddHom_apply, DirectSum.coe_decompose_mul_of_left_mem_of_le, Finsupp.toDFinsupp_coe, DirectSum.coe_mul_of_apply_of_not_le, DFinsupp.extendWith_some, DFinsupp.colex_lt_iff_of_unique, DirectSum.coe_decompose_mul_of_left_mem, DFinsupp.erase_add_single, DFinsupp.sigmaUncurry_apply, finsuppEquivDFinsupp_apply, MultilinearMap.dfinsuppFamily_smul, DFinsupp.Lex.le_iff_of_unique, DFinsupp.neLocus_neg, DFinsupp.sumAddHom_comm, DFinsupp.prod_neg_index, GradedAlgebra.proj_recompose, Submodule.mem_iSup_iff_exists_dfinsupp, DFinsupp.instIsRightCancelAdd, DFinsupp.single_injective, DFinsupp.neLocus_sub_left, DFinsupp.subset_support_tsub, DFinsupp.coe_neg, Submodule.iSup_eq_range_dfinsupp_lsum, DFinsupp.le_def, DFinsupp.instCanonicallyOrderedAddOfAddLeftMono, DFinsupp.iSup_range_lsingle, DFinsupp.mk_zero, DFinsupp.filter_smul, sigmaFinsuppEquivDFinsupp_symm_apply, MultilinearMap.fromDFinsuppEquiv_single, DFinsupp.card_Iic, DFinsupp.support_tsub, DFinsupp.filterLinearMap_apply, DFinsupp.support_eq_empty, DFinsupp.wellFoundedLT', DFinsupp.support_inf, DFinsupp.counit_comp_lsingle, DirectSum.coe_mul_apply, DirectSum.mk_apply_of_notMem, DFinsupp.single_eq_of_ne, DFinsupp.neLocus_self_sub_right, DFinsupp.infinite_of_left, DFinsupp.Colex.le_iff_of_unique, DirectSum.decompose_mul_add_left, DFinsupp.toMultiset_le_toMultiset, LinearMap.map_dfinsuppSumAddHom, DFinsupp.le_iff, DirectSum.IsInternal.ofBijective_coeLinearMap_of_mem_ne, DFinsupp.update_self, AddSubmonoid.mem_bsupr_iff_exists_dfinsupp, MvPolynomial.decompose'_apply, DFinsupp.toFinsupp_coe, MultilinearMap.freeDFinsuppEquiv_single, Module.Flat.dfinsupp_iff, DFinsupp.Colex.lt_iff, DFinsupp.wellFoundedLT, DFinsupp.comul_comp_lapply, DFinsupp.instPosSMulStrictMono, PiTensorProduct.ofDFinsuppEquiv_tprod_apply, DFinsupp.coe_add, DFinsupp.card_Ioo, MultilinearMap.freeDFinsuppEquiv_def, DFinsupp.lex_iff_of_unique, DFinsupp.mapRange.linearEquiv_apply, DFinsupp.single_neg, DFinsupp.sigmaCurry_smul, DFinsupp.support_zero, Multiset.toDFinsupp_replicate, DFinsupp.comapDomain'_apply, Multiset.uIcc_eq, DFinsupp.coe_orderEmbeddingToFun, DFinsupp.mker_mapRangeAddMonoidHom, DFinsupp.neLocus_zero_right, DFinsupp.comapDomain_smul, DFinsupp.instAddLeftReflectLE, DFinsupp.lex_fibration, DFinsupp.linearEquivFunOnFintype_symm_apply, DirectSum.coe_decompose_mul_of_right_mem_of_not_le, DFinsupp.Lex.addLeftStrictMono, DirectSum.coe_decompose_mul_of_left_mem_of_not_le, DFinsupp.equivCongrLeft_apply, DFinsupp.coe_piecewise, DFinsupp.sup_apply, DirectSum.addEquivProdDirectSum_apply, sigmaFinsuppEquivDFinsupp_smul, DFinsupp.erase_eq_sub_single, DFinsupp.prod_finset_sum_index, DFinsupp.mapRange_surjective, DFinsupp.Icc_eq, DFinsupp.Lex.addRightStrictMono, DFinsupp.bot_eq_zero, DirectSum.coe_of_mul_apply_of_not_le, DFinsupp.sum_apply, DFinsupp.mk_injective, DFinsupp.support_neg, DirectSum.addEquivProdDirectSum_symm_apply_support', DFinsupp.ker_mapRangeAddMonoidHom, DirectSum.mk_apply_of_mem, MultilinearMap.freeFinsuppEquiv_def, AddSubmonoid.iSup_eq_mrange_dfinsuppSumAddHom, DFinsupp.neLocus_sub_right, HahnEmbedding.Seed.coeff_baseEmbedding, DFinsupp.erase_def, DFinsupp.zsmul_apply, DFinsupp.toMultiset_toDFinsupp, DFinsupp.erase_sub, DFinsupp.erase_neg, DFinsupp.coe_smul, DFinsupp.coe_neLocus, DFinsupp.sumAddHom_piSingle, DFinsupp.neLocus_add_right, DFinsupp.mapRange.addEquiv_symm, DFinsupp.mapRange_zero, DFinsupp.notMem_neLocus, DFinsupp.subtypeDomain_sum, DFinsupp.nsmul_apply, DFinsupp.erase_single, DirectSum.IsInternal.ofBijective_coeLinearMap_of_mem, DFinsupp.lsum_single, DFinsupp.subtypeDomain_zero, DFinsupp.mapRange_apply, DFinsupp.single_tsub, MvPolynomial.weightedHomogeneousComponent_directSum, DFinsupp.ext_iff, DFinsupp.filter_sub, DFinsupp.toMultiset_inf, DFinsupp.subtypeSupportEqEquiv_symm_apply_coe, MultilinearMap.dfinsuppFamilyₗ_apply, MultilinearMap.dfinsupp_ext_iff, iSupIndep.linearEquiv_apply, DFinsupp.Lex.wellFounded', DFinsupp.mrange_mapRangeAddMonoidHom, DirectSum.coe_decompose_mul_of_right_mem, DFinsupp.card_uIcc, DFinsupp.comul_comp_lsingle, LinearEquiv.map_dfinsuppSumAddHom, DFinsupp.mapRange_injective, DFinsupp.filter_add, DFinsupp.add_closure_iUnion_range_single, DFinsupp.Lex.acc_single, DFinsupp.equivProdDFinsupp_add, DFinsupp.coe_update, DFinsupp.instPosSMulReflectLE, DFinsupp.sigmaCurryLEquiv_symm_apply, AddSubmonoid.bsupr_eq_mrange_dfinsuppSumAddHom, DirectSum.coe_mul_of_apply_of_mem_zero, DirectSum.of_eq_same, DFinsupp.instPosSMulMono, DFinsupp.single_add, DFinsupp.add_eq_zero_iff, MultilinearMap.dfinsuppFamily_single_left_apply, DFinsupp.instOrderedSub, instUniqueSumsDFinsupp, DirectSum.sigmaCurry_apply, DFinsupp.coprodMap_apply_single, MvPolynomial.decomposition.decompose'_apply, DFinsupp.lsum_symm_apply, DFinsupp.Lex.lt_iff_of_unique, MultilinearMap.fromDirectSumEquiv_apply, DFinsupp.filter_apply, DFinsupp.filter_zero, DFinsupp.Lex.wellFoundedLT_of_finite, DFinsupp.subtypeDomain_finsupp_sum, DFinsupp.mapRange.addEquiv_refl, PiTensorProduct.ofDFinsuppEquiv_tprod_single, DFinsupp.isScalarTower, DFinsupp.comapDomain_add, DirectSum.ext_iff, DFinsupp.sigmaUncurry_smul, DFinsupp.erase_single_same, DFinsupp.Lex.addRightMono, DirectSum.coe_decompose_mul_add_of_right_mem, DirectSum.coe_mul_of_apply_aux, TensorProduct.directSumLeft_tmul, DFinsupp.single_sub, DFinsupp.Lex.isStrictOrder, MvPolynomial.DirectSum.coeLinearMap_eq_finsum, DFinsupp.ker_mapRangeLinearMap, Finsupp.toDFinsupp_smul, DFinsupp.card_pi, DFinsupp.small, DFinsupp.instSMulPosReflectLT, DFinsupp.filter_single_neg, Finsupp.toDFinsupp_neg, DFinsupp.mem_pi, sigmaFinsuppLequivDFinsupp_symm_apply, sigmaFinsuppEquivDFinsupp_single, DFinsupp.lex_le_iff_of_unique, DFinsupp.inf_apply, DFinsupp.toMultiset_injective, DFinsupp.comapDomain_apply, DFinsupp.coeFnLinearMap_apply, DFinsupp.sumZeroHom_piSingle, DFinsupp.add_apply, DFinsupp.mapRange.addMonoidHom_apply, DFinsupp.erase_apply, DFinsupp.neLocus_eq_support_sub, DFinsupp.neLocus_zero_left, DFinsupp.support_sup_union_support_inf, DFinsupp.neg_apply, DFinsupp.lmk_apply, DFinsupp.sum_finset_sum_index, DFinsupp.erase_ne, Finsupp.toDFinsupp_sub, DFinsupp.comp_liftAddHom, DirectSum.decompose_of_mem_ne, Submodule.IsHomogeneous.mem_iff, DFinsupp.comapDomain'_smul, MultilinearMap.freeDFinsuppEquiv_apply, DFinsupp.prod_zero_index, DFinsupp.equivProdDFinsupp_symm_apply, DFinsupp.infinite_of_exists_right, DFinsupp.finset_sum_apply, Finsupp.lex_eq_invImage_dfinsupp_lex, DFinsupp.toFun_eq_coe, DFinsupp.coe_inf, Module.Free.dfinsupp, DFinsupp.neLocus_add_left, TensorProduct.directSumRight_tmul, DFinsupp.filter_neg, DirectSum.SetLike.IsHomogeneous.mem_iff, DirectSum.coeFnAddMonoidHom_apply, DFinsupp.rangeIcc_apply, DFinsupp.single_smul, DirectSum.sigmaLuncurry_apply, DFinsupp.coe_strictMono, DFinsupp.neLocus_self_add_left, DirectSum.coe_mul_of_apply_add, finsuppLEquivDirectSum_apply, DirectSum.lof_apply, DFinsupp.card_Ico, DirectSum.map_apply, DirectSum.apply_eq_component, DFinsupp.piecewise_apply, DirectSum.coe_of_mul_apply_of_le, DFinsupp.mk_add, DirectSum.coe_mul_of_apply_of_le, DFinsupp.Colex.wellFoundedLT_of_finite, DirectSum.coe_of_mul_apply_of_mem_zero, DirectSum.equivCongrLeft_apply, DFinsupp.sigmaUncurry_zero, DFinsupp.coe_sub, DFinsupp.linearEquivFunOnFintype_apply, finsuppLequivDFinsupp_apply_apply, MultilinearMap.support_dfinsuppFamily_subset, DirectSum.of_apply, DFinsupp.Lex.addLeftMono, DFinsupp.mem_rangeIcc_apply_iff, DFinsupp.single_add_erase, Multiset.toDFinsupp_injective, DirectSum.mul_eq_sum_support_ghas_mul, DFinsupp.sum_neg_index, DFinsupp.instIsLeftCancelAdd, DFinsupp.sumAddHom_apply, DFinsupp.sumAddHom_comp_single, DFinsupp.liftAddHom_singleAddHom, DirectSum.coeFnLinearMap_apply, DFinsupp.filter_single, DFinsupp.mk_of_mem, Multiset.toDFinsupp_le_toDFinsupp, Multiset.toDFinsupp_toMultiset, DFinsupp.Colex.total_le, Multiset.toDFinsupp_singleton, HahnEmbedding.Seed.hahnCoeff_apply, DFinsupp.toColex_monotone, finsuppEquivDFinsupp_symm_apply, DirectSum.coe_mul_of_apply, iSupIndep_iff_dfinsupp_lsum_injective, DirectSum.coe_mul_apply_eq_dfinsuppSum, GradedAlgebra.proj_apply, finsuppLequivDFinsupp_symm_apply, DFinsupp.support_add, DFinsupp.mk_apply, DFinsupp.coe_finset_sum, DFinsupp.coe_le_coe, DFinsupp.filter_apply_pos, DFinsupp.coe_zsmul, GradedRing.projZeroRingHom_apply, DFinsupp.subtypeDomain_apply, DFinsupp.Colex.addLeftStrictMono, sigmaFinsuppEquivDFinsupp_apply, DFinsupp.lapply_comp_lsingle_of_ne, DFinsupp.sumAddHom_zero, instIsSemisimpleModuleDFinsupp, DFinsupp.sumAddHom_singleAddHom, DFinsupp.isCentralScalar, DFinsupp.counit_single, MultilinearMap.dfinsuppFamily_zero, AddSubmonoid.mem_iSup_iff_exists_dfinsupp, Module.annihilator_dfinsupp, finsuppAddEquivDFinsupp_apply, DFinsupp.instSMulPosReflectLE, DirectSum.smul_apply, DFinsupp.sigmaCurry_zero, DFinsupp.subtypeDomain_sub, DFinsupp.Colex.addRightStrictMono, finsuppAddEquivDFinsupp_symm_apply, DFinsupp.sum_sub_index, DFinsupp.comapDomain'_add, DirectSum.IsInternal.ofBijective_coeLinearMap_of_ne, DirectSum.coe_mul_apply_eq_sum_antidiagonal, DFinsupp.instIsOrderedAddMonoid, Finsupp.toDFinsupp_zero, DFinsupp.erase_add, DFinsupp.lapply_apply, Multiset.toDFinsupp_inter, DFinsupp.Lex.wellFoundedLT, DirectSum.sigmaUncurry_apply, Module.instProjectiveDFinsupp, DirectSum.support_subset, DFinsupp.mapRange.addEquiv_trans, DFinsupp.sigmaCurry_add, DirectSum.decompose_mul_add_right, PiTensorProduct.ofDFinsuppEquiv_symm_single_tprod, Pi.comul_coe_dFinsupp, DFinsupp.mk_sub, DFinsupp.sumZeroHom_single, DFinsupp.mapRange.linearMap_id, DFinsupp.mk_of_notMem, Multiset.toDFinsupp_lt_toDFinsupp, DFinsupp.liftAddHom_comp_single, DFinsupp.mapRange.linearMap_apply, DFinsupp.comp_sumAddHom, Module.Finite.instDFinsupp, DFinsupp.Colex.isOrderedAddMonoid, DFinsupp.sumAddHom_add, Multiset.toDFinsupp_union, AddMonoidHom.dfinsuppSumAddHom_apply, DirectSum.coe_of_apply, DFinsupp.zipWith_apply, DFinsupp.Lex.acc, DFinsupp.singleAddHom_apply, RingHom.map_dfinsuppSumAddHom, DFinsupp.eq_mk_support, DirectSum.coe_decompose_mul_of_left_mem_zero, DirectSum.coe_decompose_mul_of_right_mem_of_le, DFinsupp.toFinsupp_neg, DFinsupp.toMultiset_inj, instCountableDFinsupp, DirectSum.sum_support_decompose, DFinsupp.support_inf_union_support_sup, DFinsupp.Colex.addLeftMono, PiTensorProduct.ofDirectSumEquiv_tprod_apply, Submodule.mem_biSup_iff_exists_dfinsupp, DFinsupp.subtypeDomain_neg, DFinsupp.filter_pos_add_filter_neg, DirectSum.coe_decompose_mul_of_right_mem_zero, MultilinearMap.dfinsuppFamily_single_left, DirectSum.AddSubmonoidClass.IsHomogeneous.mem_iff, DFinsupp.lapply_comp_lsingle_same, DFinsupp.toMultiset_lt_toMultiset, DFinsupp.single_eq_zero, DFinsupp.single_eq_pi_single, instTwoUniqueSumsDFinsupp, DFinsupp.lsum_apply_apply, DFinsupp.single_left_injective, DFinsupp.single_zero, DFinsupp.single_apply, DirectSum.sum_support_of, DFinsupp.finite_support, DFinsupp.mapRange.addMonoidHom_id, DFinsupp.sub_apply, DFinsupp.card_Iio, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec.image_basicOpen_eq_basicOpen, qExpansion_of_pow, DFinsupp.liftAddHom_symm_apply, DFinsupp.addHom_ext'_iff, DFinsupp.coe_nsmul, DFinsupp.support_sum, DFinsupp.coe_lt_coe, DFinsupp.card_Icc, IsHilbertSum.linearIsometryEquiv_apply_dfinsupp_sum_single, DFinsupp.subtypeDomain_smul, DFinsupp.linearIndependent_single, DFinsupp.instIsCancelAdd, DFinsupp.Lex.total_le, Finset.mem_dfinsupp_iff, DFinsupp.Lex.wellFounded_of_finite, DFinsupp.filterAddMonoidHom_apply, DirectSum.map_eq_iff, DirectSum.add_apply, iSupIndep_iff_dfinsuppSumAddHom_injective, DFinsupp.support_subset_iff, DFinsupp.comapDomain_zero, DirectSum.coe_of_mul_apply, MultilinearMap.fromDFinsuppEquiv_symm_apply, DFinsupp.equivFunOnFintype_symm_single, DFinsupp.mapRange_add, DFinsupp.Colex.isStrictOrder, DFinsupp.mk_smul, DFinsupp.sum_add_index, DirectSum.lmap_eq_iff, DFinsupp.support_smul, DFinsupp.toFinsupp_zero, DFinsupp.lhom_ext'_iff, DFinsupp.card_Ioc, GradedRing.proj_apply, DFinsupp.extendWith_none, DFinsupp.wellFoundedLT_of_finite, OrthogonalFamily.inner_right_dfinsupp, DirectSum.linearEquivFunOnFintype_symm_coe, lsum_comp_mapRange_toSpanSingleton, Multiset.toDFinsupp_inj, DirectSum.linearEquivFunOnFintype_apply, OrthogonalFamily.projection_directSum_coeAddHom, GradedRing.proj_recompose, DirectSum.zero_apply, DFinsupp.sigmaFinsetFunEquiv_apply_fst, DFinsupp.support_sup, DFinsupp.Lex.lt_iff, DFinsupp.instSMulPosStrictMono, Ideal.IsHomogeneous.mem_iff, DFinsupp.sum_single, DFinsupp.support_monotone, DFinsupp.sumAddHom_toZeroHom, DFinsupp.orderEmbeddingToFun_apply, DFinsupp.subtypeDomainAddMonoidHom_apply, DFinsupp.domLCongr_apply, DFinsupp.sigmaFinsetFunEquiv_apply_snd_coe, DFinsupp.sigmaCurry_apply, DFinsupp.coe_zero, sigmaFinsuppLequivDFinsupp_apply, DirectSum.of_eq_of_ne
|