| Metric | Count |
|---|
DefinitionsaddCommGroup, addCommMonoid, addMonoidβ, addZeroClass, addZeroClassβ, coeFnAddMonoidHom, comapDomain, comapDomain', decidableZero, equivCongrLeft, equivFunOnFintype, equivProdDFinsupp, erase, eraseAddHom, extendWith, filter, filterAddMonoidHom, hasAddβ, hasIntScalar, hasNatScalar, instAdd, instAddGroup, instAddMonoid, instDFunLike, instDecidableEq, instInhabited, instNeg, instSub, instZero, mapRange, addEquiv, addMonoidHom, mk, mkAddGroupHom, piecewise, sigmaFinsetFunEquiv, single, singleAddHom, subtypeDomain, subtypeDomainAddMonoidHom, subtypeSupportEqEquiv, support, support', toFun, unique, uniqueOfIsEmpty, update, zipWith, Β«termΞ β_,_Β» | 49 |
Theoremsadd_apply, coeFnAddMonoidHom_apply, coe_add, coe_mk', coe_neg, coe_nsmul, coe_piecewise, coe_sub, coe_update, coe_zero, coe_zsmul, comapDomain'_add, comapDomain'_apply, comapDomain'_single, comapDomain'_zero, comapDomain_add, comapDomain_apply, comapDomain_single, comapDomain_zero, eq_mk_support, equivCongrLeft_apply, equivFunOnFintype_apply, equivFunOnFintype_single, equivFunOnFintype_symm_coe, equivFunOnFintype_symm_single, equivProdDFinsupp_add, equivProdDFinsupp_apply, equivProdDFinsupp_symm_apply, eraseAddHom_apply, erase_add, erase_add_single, erase_apply, erase_def, erase_eq_sub_single, erase_ne, erase_neg, erase_same, erase_single, erase_single_ne, erase_single_same, erase_sub, erase_zero, ext, ext_iff, extendWith_none, extendWith_single_zero, extendWith_some, extendWith_zero, filterAddMonoidHom_apply, filter_add, filter_apply, filter_apply_neg, filter_apply_pos, filter_def, filter_ne_eq_erase, filter_ne_eq_erase', filter_neg, filter_pos_add_filter_neg, filter_single, filter_single_neg, filter_single_pos, filter_sub, filter_zero, finite_support, induction, inductionβ, instIsCancelAdd, instIsLeftCancelAdd, instIsRightCancelAdd, addEquiv_apply, addEquiv_refl, addEquiv_symm, addEquiv_trans, addMonoidHom_apply, addMonoidHom_comp, addMonoidHom_id, mapRange_add, mapRange_apply, mapRange_comp, mapRange_def, mapRange_id, mapRange_injective, mapRange_single, mapRange_surjective, mapRange_zero, mem_support_iff, mem_support_toFun, mk_add, mk_apply, mk_injective, mk_neg, mk_of_mem, mk_of_notMem, mk_sub, mk_zero, ne_iff, neg_apply, notMem_support_iff, nsmul_apply, piecewise_apply, piecewise_single_erase, sigmaFinsetFunEquiv_apply_fst, sigmaFinsetFunEquiv_apply_snd_coe, singleAddHom_apply, single_add, single_add_erase, single_apply, single_eq_of_ne, single_eq_of_sigma_eq, single_eq_pi_single, single_eq_same, single_eq_single_iff, single_eq_zero, single_injective, single_left_injective, single_ne_zero, single_neg, single_sub, single_zero, sub_apply, subtypeDomainAddMonoidHom_apply, subtypeDomain_add, subtypeDomain_apply, subtypeDomain_def, subtypeDomain_neg, subtypeDomain_sub, subtypeDomain_zero, subtypeSupportEqEquiv_apply_coe, subtypeSupportEqEquiv_symm_apply_coe, support_add, support_eq_empty, support_erase, support_filter, support_mapRange, support_mk'_subset, support_mk_subset, support_neg, support_single_ne_zero, support_single_subset, support_subset_iff, support_subtypeDomain, support_update, support_update_ne_zero, support_zero, support_zipWith, toFun_eq_coe, update_eq_erase, update_eq_erase_add_single, update_eq_single_add_erase, update_eq_sub_add_single, update_self, zero_apply, zipWith_apply, zipWith_def, zipWith_single_single, zsmul_apply | 156 |
| Total | 205 |
| Name | Category | Theorems |
|---|
addCommGroup π | CompOp | 1 mathmath: instIsSemisimpleModuleDFinsupp
|
addCommMonoid π | CompOp | 104 mathmath: coprodMap_apply, comul_single, Module.Flat.dfinsupp, iSupIndep.linearEquiv_symm_apply, iSupIndep.dfinsupp_lsum_injective, lsum_lsingle, linearIndependent_single_iff, lsingle_apply, MultilinearMap.fromDFinsuppEquiv_apply, instIsOrderedCancelAddMonoid, MultilinearMap.dfinsuppFamily_single, Pi.comul_comp_dFinsuppCoeFnLinearMap, Pi.counit_coe_dFinsupp, subtypeDomainLinearMap_apply, mapRange.linearEquiv_refl, Colex.isOrderedCancelAddMonoid, mapRange.linearMap_comp, mapRange.linearEquiv_trans, mapRange.linearEquiv_symm, Submodule.biSup_eq_range_dfinsupp_lsum, Lex.isOrderedCancelAddMonoid, MultilinearMap.dfinsuppFamily_apply_toFun, MultilinearMap.dfinsuppFamily_apply_support', Lex.isOrderedAddMonoid, injective_pi_lapply, range_mapRangeLinearMap, Pi.counit_comp_dFinsuppCoeFnLinearMap, sum_sum_index, sigmaCurryLEquiv_apply, instIsCocomm, MultilinearMap.dfinsuppFamily_compLinearMap_lsingle, sum_mapRange_index.linearMap, prod_sum_index, MultilinearMap.dfinsuppFamily_add, MultilinearMap.dfinsuppFamily_smul, Submodule.mem_iSup_iff_exists_dfinsupp, Submodule.iSup_eq_range_dfinsupp_lsum, iSup_range_lsingle, MultilinearMap.fromDFinsuppEquiv_single, filterLinearMap_apply, counit_comp_lsingle, MultilinearMap.freeDFinsuppEquiv_single, Module.Flat.dfinsupp_iff, comul_comp_lapply, PiTensorProduct.ofDFinsuppEquiv_tprod_apply, MultilinearMap.freeDFinsuppEquiv_def, mapRange.linearEquiv_apply, linearEquivFunOnFintype_symm_apply, prod_finset_sum_index, sum_apply, MultilinearMap.freeFinsuppEquiv_def, subtypeDomain_sum, lsum_single, MultilinearMap.dfinsuppFamilyβ_apply, MultilinearMap.dfinsupp_ext_iff, iSupIndep.linearEquiv_apply, comul_comp_lsingle, sigmaCurryLEquiv_symm_apply, MultilinearMap.dfinsuppFamily_single_left_apply, coprodMap_apply_single, lsum_symm_apply, subtypeDomain_finsupp_sum, PiTensorProduct.ofDFinsuppEquiv_tprod_single, ker_mapRangeLinearMap, sigmaFinsuppLequivDFinsupp_symm_apply, coeFnLinearMap_apply, lmk_apply, sum_finset_sum_index, MultilinearMap.freeDFinsuppEquiv_apply, finset_sum_apply, Module.Free.dfinsupp, linearEquivFunOnFintype_apply, finsuppLequivDFinsupp_apply_apply, MultilinearMap.support_dfinsuppFamily_subset, liftAddHom_singleAddHom, iSupIndep_iff_dfinsupp_lsum_injective, finsuppLequivDFinsupp_symm_apply, coe_finset_sum, lapply_comp_lsingle_of_ne, sumAddHom_singleAddHom, counit_single, MultilinearMap.dfinsuppFamily_zero, Module.annihilator_dfinsupp, instIsOrderedAddMonoid, lapply_apply, Module.instProjectiveDFinsupp, PiTensorProduct.ofDFinsuppEquiv_symm_single_tprod, Pi.comul_coe_dFinsupp, mapRange.linearMap_id, mapRange.linearMap_apply, Module.Finite.instDFinsupp, Colex.isOrderedAddMonoid, Submodule.mem_biSup_iff_exists_dfinsupp, MultilinearMap.dfinsuppFamily_single_left, lapply_comp_lsingle_same, lsum_apply_apply, support_sum, linearIndependent_single, MultilinearMap.fromDFinsuppEquiv_symm_apply, lhom_ext'_iff, lsum_comp_mapRange_toSpanSingleton, sum_single, domLCongr_apply, sigmaFinsuppLequivDFinsupp_apply
|
addMonoidβ π | CompOp | β |
addZeroClass π | CompOp | 46 mathmath: liftAddHom_apply, liftAddHom_apply_single, AddMonoidHom.map_dfinsuppSumAddHom, iSupIndep.dfinsuppSumAddHom_injective, sumAddHom_single, coeFnAddMonoidHom_apply, mapRange.addMonoidHom_comp, AddMonoidHom.coe_dfinsuppSumAddHom, AddEquiv.map_dfinsuppSumAddHom, eraseAddHom_apply, sumAddHom_comm, LinearMap.map_dfinsuppSumAddHom, AddSubmonoid.mem_bsupr_iff_exists_dfinsupp, mker_mapRangeAddMonoidHom, ker_mapRangeAddMonoidHom, AddSubmonoid.iSup_eq_mrange_dfinsuppSumAddHom, sumAddHom_piSingle, iSupIndep.linearEquiv_apply, mrange_mapRangeAddMonoidHom, LinearEquiv.map_dfinsuppSumAddHom, add_closure_iUnion_range_single, AddSubmonoid.bsupr_eq_mrange_dfinsuppSumAddHom, mapRange.addMonoidHom_apply, comp_liftAddHom, sumAddHom_apply, sumAddHom_comp_single, liftAddHom_singleAddHom, sumAddHom_zero, sumAddHom_singleAddHom, AddSubmonoid.mem_iSup_iff_exists_dfinsupp, dfinsuppSumAddHom_mem, liftAddHom_comp_single, comp_sumAddHom, sumAddHom_add, AddMonoidHom.dfinsuppSumAddHom_apply, singleAddHom_apply, RingHom.map_dfinsuppSumAddHom, Submodule.dfinsuppSumAddHom_mem, lsum_apply_apply, mapRange.addMonoidHom_id, liftAddHom_symm_apply, addHom_ext'_iff, filterAddMonoidHom_apply, iSupIndep_iff_dfinsuppSumAddHom_injective, sumAddHom_toZeroHom, subtypeDomainAddMonoidHom_apply
|
addZeroClassβ π | CompOp | β |
coeFnAddMonoidHom π | CompOp | 5 mathmath: range_mapRangeAddMonoidHom, coeFnAddMonoidHom_apply, mker_mapRangeAddMonoidHom, ker_mapRangeAddMonoidHom, mrange_mapRangeAddMonoidHom
|
comapDomain π | CompOp | 7 mathmath: equivProdDFinsupp_apply, comapDomain_smul, DirectSum.addEquivProdDirectSum_apply, comapDomain_add, comapDomain_apply, comapDomain_single, comapDomain_zero
|
comapDomain' π | CompOp | 7 mathmath: comapDomain'_zero, comapDomain'_apply, equivCongrLeft_apply, comapDomain'_smul, comapDomain'_add, comapDomain'_single, domLCongr_apply
|
decidableZero π | CompOp | β |
equivCongrLeft π | CompOp | 1 mathmath: equivCongrLeft_apply
|
equivFunOnFintype π | CompOp | 7 mathmath: equivFunOnFintype_symm_coe, equivFunOnFintype_single, equivFunOnFintype_apply, sum_eq_sum_fintype, prod_eq_prod_fintype, linearEquivFunOnFintype_symm_apply, equivFunOnFintype_symm_single
|
equivProdDFinsupp π | CompOp | 4 mathmath: equivProdDFinsupp_smul, equivProdDFinsupp_apply, equivProdDFinsupp_add, equivProdDFinsupp_symm_apply
|
erase π | CompOp | 23 mathmath: erase_single_ne, piecewise_single_erase, update_eq_erase_add_single, erase_zero, update_eq_single_add_erase, erase_same, eraseAddHom_apply, erase_add_single, support_erase, erase_eq_sub_single, erase_def, erase_sub, erase_neg, erase_single, support_update, erase_single_same, erase_apply, erase_ne, single_add_erase, filter_ne_eq_erase', erase_add, filter_ne_eq_erase, update_eq_erase
|
eraseAddHom π | CompOp | 1 mathmath: eraseAddHom_apply
|
extendWith π | CompOp | 5 mathmath: extendWith_zero, extendWith_some, equivProdDFinsupp_symm_apply, extendWith_single_zero, extendWith_none
|
filter π | CompOp | 20 mathmath: filter_apply_neg, filter_def, filter_smul, filterLinearMap_apply, AddSubmonoid.mem_bsupr_iff_exists_dfinsupp, support_filter, filter_sub, filter_add, filter_apply, filter_zero, filter_single_neg, filter_neg, filter_ne_eq_erase', filter_single, filter_apply_pos, filter_ne_eq_erase, Submodule.mem_biSup_iff_exists_dfinsupp, filter_pos_add_filter_neg, filter_single_pos, filterAddMonoidHom_apply
|
filterAddMonoidHom π | CompOp | 2 mathmath: AddSubmonoid.bsupr_eq_mrange_dfinsuppSumAddHom, filterAddMonoidHom_apply
|
hasAddβ π | CompOp | 2 mathmath: sigmaUncurry_add, sigmaCurry_add
|
hasIntScalar π | CompOp | 2 mathmath: zsmul_apply, coe_zsmul
|
hasNatScalar π | CompOp | 2 mathmath: nsmul_apply, coe_nsmul
|
instAdd π | CompOp | 60 mathmath: Finsupp.toDFinsupp_add, Multiset.equivDFinsupp_symm_apply, sigmaUncurry_add, prod_add_index, sigmaFinsuppAddEquivDFinsupp_apply, toFinsupp_add, update_eq_erase_add_single, Multiset.Icc_eq, Colex.addRightMono, sigmaFinsuppAddEquivDFinsupp_symm_apply, update_eq_single_add_erase, Multiset.equivDFinsupp_apply, neLocus_self_add_right, mapRange.addEquiv_apply, sigmaFinsuppEquivDFinsupp_add, subtypeDomain_add, update_eq_sub_add_single, erase_add_single, instIsRightCancelAdd, instCanonicallyOrderedAddOfAddLeftMono, coe_add, Multiset.uIcc_eq, instAddLeftReflectLE, Lex.addLeftStrictMono, Lex.addRightStrictMono, neLocus_add_right, mapRange.addEquiv_symm, filter_add, equivProdDFinsupp_add, single_add, add_eq_zero_iff, instOrderedSub, instUniqueSumsDFinsupp, mapRange.addEquiv_refl, comapDomain_add, Lex.addRightMono, sigmaFinsuppLequivDFinsupp_symm_apply, add_apply, neLocus_add_left, neLocus_self_add_left, mk_add, Lex.addLeftMono, single_add_erase, instIsLeftCancelAdd, support_add, Colex.addLeftStrictMono, finsuppAddEquivDFinsupp_apply, Colex.addRightStrictMono, finsuppAddEquivDFinsupp_symm_apply, comapDomain'_add, erase_add, mapRange.addEquiv_trans, sigmaCurry_add, Colex.addLeftMono, filter_pos_add_filter_neg, instTwoUniqueSumsDFinsupp, instIsCancelAdd, mapRange_add, sum_add_index, sigmaFinsuppLequivDFinsupp_apply
|
instAddGroup π | CompOp | 2 mathmath: range_mapRangeAddMonoidHom, ker_mapRangeAddMonoidHom
|
instAddMonoid π | CompOp | β |
instDFunLike π | CompOp | 233 mathmath: DirectSum.IsInternal.ofBijective_coeLinearMap_same, single_eq_same, DirectSum.bracket_apply, DirectSum.finite_support, MultilinearMap.fromDFinsuppEquiv_apply, filter_apply_neg, lex_lt_iff_of_unique, piecewise_single_erase, DirectSum.decompose_of_mem_same, Finset.mem_dfinsupp_iff_of_support_subset, equivFunOnFintype_symm_coe, mapRange_def, zero_apply, Pi.counit_coe_dFinsupp, DirectSum.lie_module_bracket_apply, DirectSum.sub_apply, coe_mono, tsub_apply, prod_eq_zero_iff, DirectSum.lequivCongrLeft_apply, DirectSum.lmap_apply, LinearMap.IsSymmetric.directSum_decompose_apply, subtypeSupportEqEquiv_apply_coe, coeFnAddMonoidHom_apply, equivFunOnFintype_apply, smul_apply, DirectSum.decompose_eq_mul_idempotent, Multiset.toDFinsupp_apply, lt_def, DirectSum.coe_of_mul_apply_aux, subtypeDomain_def, notMem_support_iff, equivProdDFinsupp_apply, MultilinearMap.dfinsuppFamily_apply_toFun, DirectSum.sum_univ_of, zipWith_def, le_iff', coe_tsub, MvPolynomial.weightedDecomposition.decompose'_apply, coe_mk', qExpansion_of_mul, AdicCompletion.sumInv_apply, lex_lt_iff, DirectSum.coe_of_mul_apply_add, lex_def, DirectSum.coe_decompose_mul_add_of_left_mem, mem_singleton_apply_iff, erase_same, coe_sup, update_eq_sub_add_single, Pi.lex_eq_dfinsupp_lex, single_le_iff, DirectSum.addEquivProdDirectSum_symm_apply_toFun, DirectSum.sigmaLcurry_apply, filter_def, DirectSum.coe_decompose_mul_of_left_mem_of_le, Finsupp.toDFinsupp_coe, DirectSum.coe_mul_of_apply_of_not_le, extendWith_some, colex_lt_iff_of_unique, DirectSum.coe_decompose_mul_of_left_mem, lex_lt_of_lt_of_preorder, erase_add_single, sigmaUncurry_apply, Lex.le_iff_of_unique, GradedAlgebra.proj_recompose, coe_neg, le_def, sigmaFinsuppEquivDFinsupp_symm_apply, card_Iic, lex_lt_of_lt, DirectSum.coe_mul_apply, DirectSum.mk_apply_of_notMem, single_eq_of_ne, Colex.le_iff_of_unique, DirectSum.decompose_mul_add_left, le_iff, DirectSum.IsInternal.ofBijective_coeLinearMap_of_mem_ne, update_self, MvPolynomial.decompose'_apply, toFinsupp_coe, MultilinearMap.freeDFinsuppEquiv_single, Colex.lt_iff, PiTensorProduct.ofDFinsuppEquiv_tprod_apply, coe_add, card_Ioo, lex_iff_of_unique, comapDomain'_apply, coe_orderEmbeddingToFun, DirectSum.coe_decompose_mul_of_right_mem_of_not_le, DirectSum.coe_decompose_mul_of_left_mem_of_not_le, coe_piecewise, sup_apply, DirectSum.addEquivProdDirectSum_apply, erase_eq_sub_single, Icc_eq, DirectSum.coe_of_mul_apply_of_not_le, sum_apply, DirectSum.mk_apply_of_mem, HahnEmbedding.Seed.coeff_baseEmbedding, erase_def, zsmul_apply, coe_smul, coe_neLocus, notMem_neLocus, nsmul_apply, DirectSum.IsInternal.ofBijective_coeLinearMap_of_mem, mapRange_apply, MvPolynomial.weightedHomogeneousComponent_directSum, ext_iff, DirectSum.coe_decompose_mul_of_right_mem, card_uIcc, coe_update, DirectSum.coe_mul_of_apply_of_mem_zero, DirectSum.of_eq_same, MultilinearMap.dfinsuppFamily_single_left_apply, DirectSum.sigmaCurry_apply, MvPolynomial.decomposition.decompose'_apply, Lex.lt_iff_of_unique, MultilinearMap.fromDirectSumEquiv_apply, filter_apply, DirectSum.ext_iff, DirectSum.coe_decompose_mul_add_of_right_mem, DirectSum.coe_mul_of_apply_aux, TensorProduct.directSumLeft_tmul, MvPolynomial.DirectSum.coeLinearMap_eq_finsum, card_pi, mem_pi, lex_le_iff_of_unique, inf_apply, comapDomain_apply, coeFnLinearMap_apply, sumZeroHom_piSingle, add_apply, erase_apply, neg_apply, erase_ne, DirectSum.decompose_of_mem_ne, Submodule.IsHomogeneous.mem_iff, MultilinearMap.freeDFinsuppEquiv_apply, finset_sum_apply, toFun_eq_coe, coe_inf, TensorProduct.directSumRight_tmul, DirectSum.SetLike.IsHomogeneous.mem_iff, DirectSum.coeFnAddMonoidHom_apply, rangeIcc_apply, DirectSum.sigmaLuncurry_apply, coe_strictMono, DirectSum.coe_mul_of_apply_add, finsuppLEquivDirectSum_apply, DirectSum.lof_apply, card_Ico, DirectSum.map_apply, DirectSum.apply_eq_component, piecewise_apply, DirectSum.coe_of_mul_apply_of_le, DirectSum.coe_mul_of_apply_of_le, DirectSum.coe_of_mul_apply_of_mem_zero, DirectSum.equivCongrLeft_apply, coe_sub, linearEquivFunOnFintype_apply, DirectSum.of_apply, mem_rangeIcc_apply_iff, single_add_erase, DirectSum.mul_eq_sum_support_ghas_mul, DirectSum.coeFnLinearMap_apply, mk_of_mem, HahnEmbedding.Seed.hahnCoeff_apply, DirectSum.coe_mul_of_apply, DirectSum.coe_mul_apply_eq_dfinsuppSum, GradedAlgebra.proj_apply, mk_apply, coe_finset_sum, coe_le_coe, filter_apply_pos, coe_zsmul, GradedRing.projZeroRingHom_apply, subtypeDomain_apply, sigmaFinsuppEquivDFinsupp_apply, DirectSum.smul_apply, DirectSum.IsInternal.ofBijective_coeLinearMap_of_ne, DirectSum.coe_mul_apply_eq_sum_antidiagonal, lapply_apply, DirectSum.sigmaUncurry_apply, DirectSum.support_subset, DirectSum.decompose_mul_add_right, Pi.comul_coe_dFinsupp, mk_of_notMem, DirectSum.coe_of_apply, zipWith_apply, eq_mk_support, DirectSum.coe_decompose_mul_of_left_mem_zero, DirectSum.coe_decompose_mul_of_right_mem_of_le, DirectSum.sum_support_decompose, PiTensorProduct.ofDirectSumEquiv_tprod_apply, DirectSum.coe_decompose_mul_of_right_mem_zero, DirectSum.AddSubmonoidClass.IsHomogeneous.mem_iff, single_eq_pi_single, single_apply, DirectSum.sum_support_of, finite_support, sub_apply, card_Iio, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec.image_basicOpen_eq_basicOpen, qExpansion_of_pow, coe_nsmul, support_sum, coe_lt_coe, card_Icc, IsHilbertSum.linearIsometryEquiv_apply_dfinsupp_sum_single, Finset.mem_dfinsupp_iff, DirectSum.map_eq_iff, DirectSum.add_apply, support_subset_iff, DirectSum.coe_of_mul_apply, DirectSum.lmap_eq_iff, card_Ioc, GradedRing.proj_apply, extendWith_none, OrthogonalFamily.inner_right_dfinsupp, DirectSum.linearEquivFunOnFintype_symm_coe, DirectSum.linearEquivFunOnFintype_apply, OrthogonalFamily.projection_directSum_coeAddHom, GradedRing.proj_recompose, DirectSum.zero_apply, Lex.lt_iff, Ideal.IsHomogeneous.mem_iff, orderEmbeddingToFun_apply, sigmaFinsetFunEquiv_apply_snd_coe, sigmaCurry_apply, coe_zero, DirectSum.of_eq_of_ne
|
instDecidableEq π | CompOp | β |
instInhabited π | CompOp | β |
instNeg π | CompOp | 14 mathmath: neLocus_neg_neg, mk_neg, neLocus_neg, prod_neg_index, coe_neg, single_neg, support_neg, erase_neg, Finsupp.toDFinsupp_neg, neg_apply, filter_neg, sum_neg_index, toFinsupp_neg, subtypeDomain_neg
|
instSub π | CompOp | 17 mathmath: neLocus_self_sub_left, toFinsupp_sub, update_eq_sub_add_single, neLocus_sub_left, neLocus_self_sub_right, erase_eq_sub_single, neLocus_sub_right, erase_sub, filter_sub, single_sub, neLocus_eq_support_sub, Finsupp.toDFinsupp_sub, coe_sub, subtypeDomain_sub, sum_sub_index, mk_sub, sub_apply
|
instZero π | CompOp | 69 mathmath: Lex.acc_zero, equivProdDFinsupp_smul, comapDomain'_zero, zero_apply, extendWith_zero, sigmaUncurry_add, sigmaUncurry_single, sum_zero_index, smul_apply, erase_zero, instSMulPosMono, smulCommClass, sigmaCurry_single, sigmaCurryLEquiv_apply, sumZeroHom_apply, toFinsupp_smul, mapRange_smul, sigmaUncurry_apply, mk_zero, filter_smul, support_eq_empty, MultilinearMap.freeDFinsuppEquiv_single, instPosSMulStrictMono, MultilinearMap.freeDFinsuppEquiv_def, sigmaCurry_smul, support_zero, neLocus_zero_right, comapDomain_smul, sigmaFinsuppEquivDFinsupp_smul, bot_eq_zero, coe_smul, mapRange_zero, erase_single, subtypeDomain_zero, instPosSMulReflectLE, sigmaCurryLEquiv_symm_apply, instPosSMulMono, add_eq_zero_iff, filter_zero, isScalarTower, sigmaUncurry_smul, erase_single_same, Finsupp.toDFinsupp_smul, instSMulPosReflectLT, filter_single_neg, sumZeroHom_piSingle, neLocus_zero_left, comapDomain'_smul, MultilinearMap.freeDFinsuppEquiv_apply, prod_zero_index, single_smul, sigmaUncurry_zero, filter_single, isCentralScalar, instSMulPosReflectLE, sigmaCurry_zero, Finsupp.toDFinsupp_zero, sigmaCurry_add, sumZeroHom_single, single_eq_zero, single_zero, subtypeDomain_smul, comapDomain_zero, mk_smul, support_smul, toFinsupp_zero, instSMulPosStrictMono, sigmaCurry_apply, coe_zero
|
mapRange π | CompOp | 20 mathmath: coprodMap_apply, mapRange_def, mapRange.addEquiv_apply, mapRange_smul, mapRange_single, mapRange_id, mapRange.linearEquiv_apply, mapRange_surjective, mapRange_zero, mapRange_apply, mapRange_injective, mapRange.addMonoidHom_apply, mapRange_comp, sum_mapRange_index, mapRange_neLocus_eq, prod_mapRange_index, mapRange.linearMap_apply, support_mapRange, mapRange_add, subset_mapRange_neLocus
|
mk π | CompOp | β |
mkAddGroupHom π | CompOp | β |
piecewise π | CompOp | 4 mathmath: piecewise_single_erase, lex_fibration, coe_piecewise, piecewise_apply
|
sigmaFinsetFunEquiv π | CompOp | 2 mathmath: sigmaFinsetFunEquiv_apply_fst, sigmaFinsetFunEquiv_apply_snd_coe
|
single π | CompOp | 72 mathmath: comul_single, iSupIndep.linearEquiv_symm_apply, single_eq_same, linearIndependent_single_iff, lsingle_apply, prod_single_index, MultilinearMap.dfinsuppFamily_single, erase_single_ne, piecewise_single_erase, liftAddHom_apply_single, extendWith_zero, sigmaUncurry_single, equivFunOnFintype_single, update_eq_erase_add_single, zipWith_single_single, sumAddHom_single, update_eq_single_add_erase, toMultiset_single, sigmaCurry_single, single_eq_single_iff, update_eq_sub_add_single, single_le_iff, mapRange_single, erase_add_single, single_injective, MultilinearMap.fromDFinsuppEquiv_single, single_eq_of_ne, MultilinearMap.freeDFinsuppEquiv_single, single_neg, Multiset.toDFinsupp_replicate, toFinsupp_single, erase_eq_sub_single, single_eq_of_sigma_eq, erase_single, lsum_single, single_tsub, add_closure_iUnion_range_single, Lex.acc_single, single_add, DirectSum.single_eq_lof, MultilinearMap.dfinsuppFamily_single_left_apply, coprodMap_apply_single, PiTensorProduct.ofDFinsuppEquiv_tprod_single, erase_single_same, single_sub, filter_single_neg, sigmaFinsuppEquivDFinsupp_single, MultilinearMap.freeDFinsuppEquiv_apply, single_smul, single_add_erase, filter_single, support_single_subset, Multiset.toDFinsupp_singleton, sum_single_index, counit_single, extendWith_single_zero, PiTensorProduct.ofDFinsuppEquiv_symm_single_tprod, sumZeroHom_single, Finsupp.toDFinsupp_single, singleAddHom_apply, single_eq_zero, single_eq_pi_single, single_left_injective, single_zero, support_single_ne_zero, single_apply, comapDomain_single, linearIndependent_single, filter_single_pos, comapDomain'_single, equivFunOnFintype_symm_single, sum_single
|
singleAddHom π | CompOp | 7 mathmath: sumAddHom_comp_single, liftAddHom_singleAddHom, sumAddHom_singleAddHom, liftAddHom_comp_single, singleAddHom_apply, liftAddHom_symm_apply, addHom_ext'_iff
|
subtypeDomain π | CompOp | 14 mathmath: subtypeDomainLinearMap_apply, support_subtypeDomain, subtypeDomain_def, subtypeDomain_add, sum_subtypeDomain_index, subtypeDomain_sum, subtypeDomain_zero, subtypeDomain_finsupp_sum, prod_subtypeDomain_index, subtypeDomain_apply, subtypeDomain_sub, subtypeDomain_neg, subtypeDomain_smul, subtypeDomainAddMonoidHom_apply
|
subtypeDomainAddMonoidHom π | CompOp | 1 mathmath: subtypeDomainAddMonoidHom_apply
|
subtypeSupportEqEquiv π | CompOp | 2 mathmath: subtypeSupportEqEquiv_apply_coe, subtypeSupportEqEquiv_symm_apply_coe
|
support π | CompOp | 76 mathmath: support_zipWith, support_mono, sigmaFinsuppEquivDFinsupp_support, MultilinearMap.fromDFinsuppEquiv_apply, Multiset.toDFinsupp_support, mapRange_def, disjoint_iff, support_subtypeDomain, prod_eq_zero_iff, neLocus_self_sub_left, subtypeSupportEqEquiv_apply_coe, mem_support_toFun, subtypeDomain_def, notMem_support_iff, zipWith_def, toDFinsupp_support, DirectSum.support_of, support_mk_subset, neLocus_self_add_right, filter_def, support_erase, subset_support_tsub, card_Iic, support_tsub, support_eq_empty, support_inf, DirectSum.coe_mul_apply, neLocus_self_sub_right, support_rangeIcc_subset, support_mk'_subset, card_Ioo, support_filter, support_zero, neLocus_zero_right, support_update_ne_zero, Icc_eq, support_neg, erase_def, GradedRing.mem_support_iff, subtypeSupportEqEquiv_symm_apply_coe, support_update, mem_support_iff, card_uIcc, MultilinearMap.fromDirectSumEquiv_apply, neLocus_eq_support_sub, neLocus_zero_left, support_sup_union_support_inf, neLocus_self_add_left, card_Ico, DirectSum.support_of_subset, MultilinearMap.support_dfinsuppFamily_subset, toFinsupp_support, DirectSum.mul_eq_sum_support_ghas_mul, support_single_subset, support_add, DirectSum.support_smul, DirectSum.support_zero, DirectSum.support_subset, eq_mk_support, DirectSum.sum_support_decompose, support_inf_union_support_sup, GradedAlgebra.mem_support_iff, support_single_ne_zero, DirectSum.sum_support_of, card_Iio, support_sum, card_Icc, support_mapRange, Finset.mem_dfinsupp_iff, support_subset_iff, support_smul, card_Ioc, sigmaFinsetFunEquiv_apply_fst, support_sup, support_monotone, sigmaFinsetFunEquiv_apply_snd_coe
|
support' π | CompOp | 2 mathmath: MultilinearMap.dfinsuppFamily_apply_support', DirectSum.addEquivProdDirectSum_symm_apply_support'
|
toFun π | CompOp | 1 mathmath: toFun_eq_coe
|
unique π | CompOp | β |
uniqueOfIsEmpty π | CompOp | β |
update π | CompOp | 8 mathmath: update_eq_erase_add_single, update_eq_single_add_erase, update_eq_sub_add_single, update_self, support_update_ne_zero, support_update, coe_update, update_eq_erase
|
zipWith π | CompOp | 6 mathmath: support_zipWith, zipWith_single_single, zipWith_def, zipWith_neLocus_eq_right, zipWith_apply, zipWith_neLocus_eq_left
|