Basic

📁 Source: Mathlib/Data/Finsupp/Basic.lean

Statistics

Metric	Count
Definitions `comapDomain`, `addMonoidHom`, `curry`, `curryAddEquiv`, `curryEquiv`, `domCongr`, `equivCongrLeft`, `equivMapDomain`, `extendDomain`, `filter`, `filterAddHom`, `finsuppProdEquiv`, `frange`, `graph`, `mapDomain`, `addMonoidHom`, `mapDomainEmbedding`, `piecewise`, `restrictSupportEquiv`, `sigmaFinsuppAddEquivPiFinsupp`, `sigmaFinsuppEquivPiFinsupp`, `split`, `splitComp`, `splitSupport`, `subtypeDomain`, `subtypeDomainAddMonoidHom`, `sumElim`, `sumFinsuppAddEquivProdFinsupp`, `sumFinsuppEquivProdFinsupp`, `uncurry`, `uniqueOfLeft`, `uniqueOfRight`	32
Theorems `apply_eq_of_mem_graph`, `coe_curryAddEquiv`, `coe_sumElim`, `addMonoidHom_apply`, `comapDomain_add`, `comapDomain_add_of_injective`, `comapDomain_apply`, `comapDomain_mapDomain`, `comapDomain_single`, `comapDomain_support`, `comapDomain_surjective`, `comapDomain_zero`, `curryAddEquiv_symm_apply`, `curryEquiv_apply`, `curryEquiv_symm_apply`, `curry_apply`, `curry_single`, `curry_uncurry`, `domCongr_apply`, `domCongr_refl`, `domCongr_symm`, `domCongr_trans`, `embDomain_comapDomain`, `embDomain_eq_mapDomain`, `eq_zero_of_comapDomain_eq_zero`, `equivCongrLeft_apply`, `equivCongrLeft_symm`, `equivMapDomain_apply`, `equivMapDomain_eq_mapDomain`, `equivMapDomain_refl`, `equivMapDomain_refl'`, `equivMapDomain_single`, `equivMapDomain_symm_apply`, `equivMapDomain_trans`, `equivMapDomain_trans'`, `equivMapDomain_zero`, `extendDomain_apply`, `extendDomain_eq_embDomain_subtype`, `extendDomain_single`, `extendDomain_subtypeDomain`, `extendDomain_support`, `extendDomain_toFun`, `filter_add`, `filter_apply`, `filter_apply_neg`, `filter_apply_pos`, `filter_curry`, `filter_eq_indicator`, `filter_eq_self_iff`, `filter_eq_sum`, `filter_eq_zero_iff`, `filter_neg`, `filter_pos_add_filter_neg`, `filter_single_of_neg`, `filter_single_of_pos`, `filter_sub`, `filter_sum`, `filter_zero`, `finite_range`, `frange_single`, `fst_sumFinsuppAddEquivProdFinsupp`, `fst_sumFinsuppEquivProdFinsupp`, `graph_eq_empty`, `graph_inj`, `graph_injective`, `graph_zero`, `image_fst_graph`, `addMonoidHom_apply`, `addMonoidHom_comp`, `addMonoidHom_comp_mapRange`, `addMonoidHom_id`, `mapDomainEmbedding_apply`, `mapDomain_add`, `mapDomain_apply`, `mapDomain_apply'`, `mapDomain_comapDomain`, `mapDomain_comapDomain_nat_add_one`, `mapDomain_comp`, `mapDomain_congr`, `mapDomain_equiv_apply`, `mapDomain_finset_sum`, `mapDomain_id`, `mapDomain_injOn`, `mapDomain_injective`, `mapDomain_mapRange`, `mapDomain_notin_range`, `mapDomain_single`, `mapDomain_sum`, `mapDomain_support`, `mapDomain_support_of_injOn`, `mapDomain_support_of_injective`, `mapDomain_surjective`, `mapDomain_zero`, `mapRange_finset_sum`, `mapRange_multiset_sum`, `mem_frange`, `mem_frange_of_mem`, `mem_graph_iff`, `mem_range_mapDomain_iff`, `mem_splitSupport_iff_nonzero`, `mem_support_finset_sum`, `mem_support_multiset_sum`, `mk_mem_graph`, `mk_mem_graph_iff`, `notMem_graph_snd_zero`, `piecewise_apply`, `piecewise_support`, `prod_div_prod_filter`, `prod_equivMapDomain`, `prod_filter_index`, `prod_filter_mul_prod_filter_not`, `prod_mapDomain_index`, `prod_mapDomain_index_inj`, `prod_subtypeDomain_index`, `prod_sumElim`, `range_subset_insert_frange`, `restrictSupportEquiv_apply`, `restrictSupportEquiv_symm_apply_coe`, `restrictSupportEquiv_symm_single`, `sigmaFinsuppAddEquivPiFinsupp_apply`, `sigmaFinsuppEquivPiFinsupp_apply`, `sigma_sum`, `sigma_support`, `snd_sumFinsuppAddEquivProdFinsupp`, `snd_sumFinsuppEquivProdFinsupp`, `split_apply`, `subtypeDomain_add`, `subtypeDomain_apply`, `subtypeDomain_eq_iff`, `subtypeDomain_eq_iff_forall`, `subtypeDomain_eq_zero_iff`, `subtypeDomain_eq_zero_iff'`, `subtypeDomain_extendDomain`, `subtypeDomain_finsupp_sum`, `subtypeDomain_neg`, `subtypeDomain_not_piecewise`, `subtypeDomain_piecewise`, `subtypeDomain_sub`, `subtypeDomain_sum`, `subtypeDomain_zero`, `sumElim_apply`, `sumElim_inl`, `sumElim_inr`, `sumElim_support`, `sumFinsuppAddEquivProdFinsupp_apply`, `sumFinsuppAddEquivProdFinsupp_symm_apply`, `sumFinsuppAddEquivProdFinsupp_symm_inl`, `sumFinsuppAddEquivProdFinsupp_symm_inr`, `sumFinsuppEquivProdFinsupp_apply`, `sumFinsuppEquivProdFinsupp_symm_apply`, `sumFinsuppEquivProdFinsupp_symm_inl`, `sumFinsuppEquivProdFinsupp_symm_inr`, `sum_comapDomain`, `sum_curry_index`, `sum_equivMapDomain`, `sum_filter_add_sum_filter_not`, `sum_filter_index`, `sum_mapDomain_index`, `sum_mapDomain_index_addMonoidHom`, `sum_mapDomain_index_inj`, `sum_sub_sum_filter`, `sum_subtypeDomain_index`, `sum_sumElim`, `sum_uncurry_index`, `sum_uncurry_index'`, `sum_update_add`, `support_curry`, `support_extendDomain_subset`, `support_filter`, `support_subtypeDomain`, `uncurry_apply`, `uncurry_apply_pair`, `uncurry_curry`, `uncurry_single`, `zero_notMem_frange`, `cast_finsuppProd`, `cast_finsupp_sum`, `cast_finsuppProd`, `cast_finsupp_sum`, `cast_finsuppProd`, `cast_finsupp_sum`	181
Total	213

Finsupp

Definitions

Name	Category	Theorems
`comapDomain` 📖	CompOp	19 math math: `comapDomain_add`, `comapDomain_smul_of_injective`, `comapDomain_zero`, `Polynomial.derivativeFinsupp_derivative`, `embDomain_comapDomain`, `mapDomain_comapDomain`, `comapDomain_single`, `comapDomain_surjective`, `comapDomain_mapDomain`, `lcomapDomain_apply`, `comapDomain_apply`, `sumFinsuppAddEquivProdFinsupp_apply`, `sum_comapDomain`, `comapDomain_smul`, `comapDomain.addMonoidHom_apply`, `comapDomain_support`, `linearCombination_comapDomain`, `comapDomain_add_of_injective`, `sumFinsuppEquivProdFinsupp_apply`
`curry` 📖	CompOp	10 math math: `curryEquiv_apply`, `filter_curry`, `curry_single`, `coe_curryAddEquiv`, `uncurry_curry`, `sum_curry_index`, `curryLinearEquiv_apply`, `curry_uncurry`, `support_curry`, `curry_apply`
`curryAddEquiv` 📖	CompOp	2 math math: `coe_curryAddEquiv`, `curryAddEquiv_symm_apply`
`curryEquiv` 📖	CompOp	2 math math: `curryEquiv_apply`, `curryEquiv_symm_apply`
`domCongr` 📖	CompOp	5 math math: `domCongr_refl`, `domCongr_apply`, `domCongr_symm`, `domLCongr_apply`, `domCongr_trans`
`equivCongrLeft` 📖	CompOp	2 math math: `equivCongrLeft_apply`, `equivCongrLeft_symm`
`equivMapDomain` 📖	CompOp	20 math math: `equivCongrLeft_apply`, `equivMapDomain_single`, `MonoidAlgebra.opRingEquiv_symm_apply`, `sum_equivMapDomain`, `AddMonoidAlgebra.opRingEquiv_symm_apply`, `domCongr_apply`, `prod_equivMapDomain`, `LinearIndependent.span_repr_eq`, `equivMapDomain_trans'`, `equivMapDomain_zero`, `equivMapDomain_eq_mapDomain`, `SkewMonoidAlgebra.toFinsupp_equivMapDomain`, `equivMapDomain_symm_apply`, `equivMapDomain_refl`, `equivMapDomain_apply`, `AddMonoidAlgebra.opRingEquiv_apply`, `linearCombination_equivMapDomain`, `equivMapDomain_trans`, `equivMapDomain_refl'`, `MonoidAlgebra.opRingEquiv_apply`
`extendDomain` 📖	CompOp	10 math math: `support_extendDomain_subset`, `extendDomain_subtypeDomain`, `subtypeDomain_extendDomain`, `extendDomain_single`, `extendDomain_eq_embDomain_subtype`, `extendDomain_toFun`, `supportedEquivFinsupp_symm_apply_coe`, `extendDomain_support`, `extendDomain_apply`, `restrictSupportEquiv_symm_apply_coe`
`filter` 📖	CompOp	26 math math: `restrictDom_apply`, `filter_smul`, `filter_apply_neg`, `filter_apply_pos`, `filter_eq_indicator`, `filter_neg`, `sum_sub_sum_filter`, `filter_sum`, `filter_curry`, `sum_filter_add_sum_filter_not`, `filter_add`, `filter_sub`, `sum_filter_index`, `filter_eq_sum`, `filter_eq_zero_iff`, `prod_filter_mul_prod_filter_not`, `prod_filter_index`, `filter_single_of_neg`, `filter_apply`, `prod_div_prod_filter`, `filter_pos_add_filter_neg`, `filter_single_of_pos`, `filter_eq_self_iff`, `support_filter`, `Polynomial.IsUnitTrinomial.irreducible_aux1`, `filter_zero`
`filterAddHom` 📖	CompOp	—
`finsuppProdEquiv` 📖	CompOp	—
`frange` 📖	CompOp	5 math math: `range_subset_insert_frange`, `mem_frange_of_mem`, `frange_single`, `zero_notMem_frange`, `mem_frange`
`graph` 📖	CompOp	10 math math: `graph_inj`, `mk_mem_graph_iff`, `mk_mem_graph`, `notMem_graph_snd_zero`, `toAList_entries`, `graph_zero`, `image_fst_graph`, `graph_eq_empty`, `mem_graph_iff`, `graph_injective`
`mapDomain` 📖	CompOp	55 math math: `groupHomology.chainsMap_f_3_comp_chainsIso₃_apply`, `mapDomain_nonneg`, `mapDomain_comapDomain_nat_add_one`, `sum_mapDomain_index_inj`, `mem_range_mapDomain_iff`, `mapDomain_support_of_injective`, `mapDomain_support_of_injOn`, `mapDomain_mapRange`, `mapDomain_support`, `mapDomain_nonpos`, `mapDomain_surjective`, `mapDomain.coe_linearEquiv`, `MvPolynomial.support_rename_of_injective`, `mapDomain_injOn`, `sum_mapDomain_index`, `leftInverse_lcomapDomain_mapDomain`, `mapDomain_single`, `mapDomain_mono`, `mapDomain_comapDomain`, `Module.Basis.repr_reindex`, `comapDomain_mapDomain`, `mapDomain_zero`, `mapDomainEmbedding_apply`, `MvPolynomial.coeff_rename_mapDomain`, `prod_mapDomain_index_inj`, `mapDomain_id`, `mapDomain_congr`, `mapDomain_apply`, `TopModuleCat.freeMap_map`, `MvPolynomial.rename_monomial`, `equivMapDomain_eq_mapDomain`, `linearCombination_mapDomain`, `comapSMul_def`, `mapDomain_finset_sum`, `coe_lmapDomain`, `SkewMonoidAlgebra.toFinsupp_mapDomain`, `prod_mapDomain_index`, `mapDomain_equiv_apply`, `mapDomain.addMonoidHom_apply`, `embDomain_eq_mapDomain`, `mapDomain_comp`, `mapDomain_sum`, `mapDomain_apply'`, `mapDomain_add`, `Algebra.Generators.comp_σ`, `MvPolynomial.coeff_rename_ne_zero`, `toMultiset_map`, `mapDomain_smul`, `groupHomology.chainsMap_f_1_comp_chainsIso₁_apply`, `mapDomain_injective`, `sum_mapDomain_index_addMonoidHom`, `MvPolynomial.rename_eq`, `lmapDomain_apply`, `groupHomology.chainsMap_f_2_comp_chainsIso₂_apply`, `mapDomain_notin_range`
`mapDomainEmbedding` 📖	CompOp	1 math math: `mapDomainEmbedding_apply`
`piecewise` 📖	CompOp	4 math math: `piecewise_apply`, `subtypeDomain_piecewise`, `piecewise_support`, `subtypeDomain_not_piecewise`
`restrictSupportEquiv` 📖	CompOp	3 math math: `restrictSupportEquiv_symm_single`, `restrictSupportEquiv_apply`, `restrictSupportEquiv_symm_apply_coe`
`sigmaFinsuppAddEquivPiFinsupp` 📖	CompOp	1 math math: `sigmaFinsuppAddEquivPiFinsupp_apply`
`sigmaFinsuppEquivPiFinsupp` 📖	CompOp	1 math math: `sigmaFinsuppEquivPiFinsupp_apply`
`split` 📖	CompOp	6 math math: `sigma_sum`, `split_embSigma_of_ne`, `split_apply`, `sigmaFinsuppEquivDFinsupp_apply`, `sigma_support`, `split_embSigma_self`
`splitComp` 📖	CompOp	—
`splitSupport` 📖	CompOp	4 math math: `sigmaFinsuppEquivDFinsupp_support`, `sigma_sum`, `sigma_support`, `mem_splitSupport_iff_nonzero`
`subtypeDomain` 📖	CompOp	20 math math: `subtypeDomain_add`, `subtypeDomain_neg`, `extendDomain_subtypeDomain`, `subtypeDomain_extendDomain`, `subtypeDomain_finsupp_sum`, `subtypeDomain_apply`, `support_subtypeDomain`, `subtypeDomain_eq_zero_iff'`, `subtypeDomain_piecewise`, `subtypeDomain_eq_iff_forall`, `subtypeDomain_eq_zero_iff`, `sum_subtypeDomain_index`, `prod_subtypeDomain_index`, `restrictSupportEquiv_apply`, `subtypeDomain_eq_iff`, `subtypeDomain_not_piecewise`, `subtypeDomain_sub`, `subtypeDomain_sum`, `subtypeDomain_zero`, `lsubtypeDomain_apply`
`subtypeDomainAddMonoidHom` 📖	CompOp	—
`sumElim` 📖	CompOp	11 math math: `coe_sumElim`, `sumElim_inr`, `sumElim_apply`, `sumElim_support`, `sumFinsuppAddEquivProdFinsupp_symm_apply`, `prod_sumElim`, `sumFinsuppEquivProdFinsupp_symm_apply`, `Algebra.Generators.toComp_toAlgHom_monomial`, `sum_sumElim`, `Algebra.Generators.ofComp_toAlgHom_monomial_sumElim`, `sumElim_inl`
`sumFinsuppAddEquivProdFinsupp` 📖	CompOp	8 math math: `sumFinsuppLEquivProdFinsupp_apply`, `sumFinsuppAddEquivProdFinsupp_symm_inl`, `sumFinsuppAddEquivProdFinsupp_symm_apply`, `sumFinsuppLEquivProdFinsupp_symm_apply`, `snd_sumFinsuppAddEquivProdFinsupp`, `sumFinsuppAddEquivProdFinsupp_apply`, `fst_sumFinsuppAddEquivProdFinsupp`, `sumFinsuppAddEquivProdFinsupp_symm_inr`
`sumFinsuppEquivProdFinsupp` 📖	CompOp	6 math math: `sumFinsuppEquivProdFinsupp_symm_inr`, `fst_sumFinsuppEquivProdFinsupp`, `sumFinsuppEquivProdFinsupp_symm_apply`, `sumFinsuppEquivProdFinsupp_symm_inl`, `snd_sumFinsuppEquivProdFinsupp`, `sumFinsuppEquivProdFinsupp_apply`
`uncurry` 📖	CompOp	10 math math: `uncurry_apply`, `uncurry_single`, `uncurry_curry`, `sum_uncurry_index'`, `sum_uncurry_index`, `uncurry_apply_pair`, `curryEquiv_symm_apply`, `curryAddEquiv_symm_apply`, `curry_uncurry`, `curryLinearEquiv_symm_apply`
`uniqueOfLeft` 📖	CompOp	—
`uniqueOfRight` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_eq_of_mem_graph` 📖	mathematical	`Finset` `Finset.instMembership` `graph`	`DFunLike.coe` `Finsupp` `instFunLike`	—	`mem_graph_iff`
`coe_curryAddEquiv` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `instZero` `instAdd` `instAddZeroClass` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `curryAddEquiv` `curry`	—	—
`coe_sumElim` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `instFunLike` `sumElim`	—	—
`comapDomain_add` 📖	mathematical	`Set.InjOn` `Set.preimage` `SetLike.coe` `Finset` `Finset.instSetLike` `support` `AddZero.toZero` `AddZeroClass.toAddZero` `Finsupp` `instAdd`	`comapDomain`	—	`ext`
`comapDomain_add_of_injective` 📖	mathematical	—	`comapDomain` `AddZero.toZero` `AddZeroClass.toAddZero` `Finsupp` `instAdd` `Function.Injective.injOn` `Set.preimage` `SetLike.coe` `Finset` `Finset.instSetLike` `support`	—	`comapDomain_add` `Function.Injective.injOn`
`comapDomain_apply` 📖	mathematical	`Set.InjOn` `Set.preimage` `SetLike.coe` `Finset` `Finset.instSetLike` `support`	`DFunLike.coe` `Finsupp` `instFunLike` `comapDomain`	—	—
`comapDomain_mapDomain` 📖	mathematical	—	`comapDomain` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `mapDomain` `Function.Injective.injOn` `Set.preimage` `SetLike.coe` `Finset` `Finset.instSetLike` `support`	—	`ext` `Function.Injective.injOn` `comapDomain_apply` `mapDomain_apply`
`comapDomain_single` 📖	mathematical	`Set.InjOn` `Set.preimage` `SetLike.coe` `Finset` `Finset.instSetLike` `support` `single`	`comapDomain`	—	`eq_or_ne` `single_zero` `comapDomain.congr_simp` `comapDomain_zero` `eq_single_iff` `comapDomain_apply` `comapDomain_support` `Finset.coe_subset` `Finset.coe_preimage` `support_single_ne_zero` `Finset.coe_singleton` `single_eq_same`
`comapDomain_support` 📖	mathematical	`Set.InjOn` `Set.preimage` `SetLike.coe` `Finset` `Finset.instSetLike` `support`	`comapDomain` `Finset.preimage`	—	—
`comapDomain_surjective` 📖	mathematical	—	`Finsupp` `comapDomain` `Function.Injective.injOn` `Set.preimage` `SetLike.coe` `Finset` `Finset.instSetLike` `support`	—	`isEmpty_or_nonempty` `Function.Injective.injOn` `ext` `Function.Injective.hasLeftInverse`
`comapDomain_zero` 📖	mathematical	`Set.InjOn` `Set.preimage` `SetLike.coe` `Finset` `Finset.instSetLike` `support` `Finsupp` `instZero` `Set` `Set.instEmptyCollection` `Set.injOn_empty` `Finset.instEmptyCollection` `Finset.coe_empty`	`comapDomain`	—	`ext`
`curryAddEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `instZero` `instAdd` `instAddZeroClass` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `curryAddEquiv` `uncurry`	—	—
`curryEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Finsupp` `instZero` `EquivLike.toFunLike` `Equiv.instEquivLike` `curryEquiv` `curry`	—	—
`curryEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Finsupp` `instZero` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `curryEquiv` `uncurry`	—	—
`curry_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `instFunLike` `instZero` `curry`	—	—
`curry_single` 📖	mathematical	—	`curry` `single` `Finsupp` `instZero`	—	`curry_uncurry` `uncurry_single`
`curry_uncurry` 📖	mathematical	—	`curry` `uncurry`	—	`ext`
`domCongr_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAdd` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `domCongr` `equivMapDomain`	—	—
`domCongr_refl` 📖	mathematical	—	`domCongr` `Equiv.refl` `AddEquiv.refl` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAdd`	—	`AddEquiv.ext` `equivMapDomain_refl`
`domCongr_symm` 📖	mathematical	—	`AddEquiv.symm` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAdd` `domCongr` `Equiv.symm`	—	`AddEquiv.ext`
`domCongr_trans` 📖	mathematical	—	`AddEquiv.trans` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAdd` `domCongr` `Equiv.trans`	—	`AddEquiv.ext` `equivMapDomain_trans`
`embDomain_comapDomain` 📖	mathematical	`Set` `Set.instHasSubset` `SetLike.coe` `Finset` `Finset.instSetLike` `support` `Set.range` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding`	`embDomain` `comapDomain` `Function.Injective.injOn` `Function.Embedding.injective` `Set.preimage`	—	`ext` `Function.Injective.injOn` `Function.Embedding.injective` `embDomain_apply_self` `comapDomain_apply` `notMem_support_iff` `embDomain_notin_range`
`embDomain_eq_mapDomain` 📖	mathematical	—	`embDomain` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `mapDomain` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding`	—	`ext` `mapDomain_apply` `Function.Embedding.injective` `embDomain_apply_self` `mapDomain_notin_range` `embDomain_notin_range`
`eq_zero_of_comapDomain_eq_zero` 📖	—	`Set.BijOn` `Set.preimage` `SetLike.coe` `Finset` `Finset.instSetLike` `support` `comapDomain` `Set.BijOn.injOn` `Finsupp` `instZero`	—	—	`Set.BijOn.injOn` `support_eq_empty` `comapDomain.eq_1`
`equivCongrLeft_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Finsupp` `EquivLike.toFunLike` `Equiv.instEquivLike` `equivCongrLeft` `equivMapDomain`	—	—
`equivCongrLeft_symm` 📖	mathematical	—	`Equiv.symm` `Finsupp` `equivCongrLeft`	—	—
`equivMapDomain_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `instFunLike` `equivMapDomain` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm`	—	—
`equivMapDomain_eq_mapDomain` 📖	mathematical	—	`equivMapDomain` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `mapDomain` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`ext` `mapDomain_equiv_apply`
`equivMapDomain_refl` 📖	mathematical	—	`equivMapDomain` `Equiv.refl`	—	`ext`
`equivMapDomain_refl'` 📖	mathematical	—	`equivMapDomain` `Equiv.refl` `Finsupp`	—	`ext`
`equivMapDomain_single` 📖	mathematical	—	`equivMapDomain` `single` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`ext` `single_apply`
`equivMapDomain_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `instFunLike` `equivMapDomain` `Equiv.symm` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	—
`equivMapDomain_trans` 📖	mathematical	—	`equivMapDomain` `Equiv.trans`	—	`ext`
`equivMapDomain_trans'` 📖	mathematical	—	`equivMapDomain` `Equiv.trans` `Finsupp`	—	`ext`
`equivMapDomain_zero` 📖	mathematical	—	`equivMapDomain` `Finsupp` `instZero`	—	`ext`
`extendDomain_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `instFunLike` `extendDomain`	—	—
`extendDomain_eq_embDomain_subtype` 📖	mathematical	—	`extendDomain` `embDomain` `Function.Embedding.subtype`	—	`ext` `embDomain_apply_self` `instIsEmptyFalse`
`extendDomain_single` 📖	mathematical	—	`extendDomain` `single`	—	`ext` `eq_or_ne` `Subtype.prop` `Subtype.coe_eta`
`extendDomain_subtypeDomain` 📖	mathematical	—	`extendDomain` `subtypeDomain`	—	`ext`
`extendDomain_support` 📖	mathematical	—	`support` `extendDomain` `Finset.map` `Function.Embedding.subtype`	—	`Finset.disjUnion_empty`
`extendDomain_toFun` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `instFunLike` `extendDomain`	—	`extendDomain_apply`
`filter_add` 📖	mathematical	—	`filter` `AddZero.toZero` `AddZeroClass.toAddZero` `Finsupp` `instAdd`	—	`AddMonoidHom.map_add`
`filter_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `instFunLike` `filter`	—	—
`filter_apply_neg` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `instFunLike` `filter`	—	—
`filter_apply_pos` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `instFunLike` `filter`	—	—
`filter_curry` 📖	mathematical	—	`curry` `filter` `Finsupp` `instZero`	—	`ext`
`filter_eq_indicator` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `instFunLike` `filter` `Set.indicator` `setOf`	—	`Set.indicator_apply`
`filter_eq_self_iff` 📖	mathematical	—	`filter`	—	`filter_eq_indicator`
`filter_eq_sum` 📖	mathematical	—	`filter` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finset.sum` `Finsupp` `instAddCommMonoid` `Finset.filter` `support` `single` `DFunLike.coe` `instFunLike`	—	`sum_single` `Finset.sum_congr` `filter_apply_pos` `Finset.mem_filter`
`filter_eq_zero_iff` 📖	mathematical	—	`filter` `Finsupp` `instZero` `DFunLike.coe` `instFunLike`	—	`filter_eq_indicator`
`filter_neg` 📖	mathematical	—	`filter` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Finsupp` `instNeg`	—	`AddMonoidHom.map_neg`
`filter_pos_add_filter_neg` 📖	mathematical	—	`Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `instAdd` `filter`	—	`DFunLike.coe_injective` `filter_eq_indicator` `Set.indicator_self_add_compl`
`filter_single_of_neg` 📖	mathematical	—	`filter` `single` `Finsupp` `instZero`	—	`filter_eq_zero_iff` `single_apply_eq_zero`
`filter_single_of_pos` 📖	mathematical	—	`filter` `single`	—	`filter_eq_self_iff` `single_apply_ne_zero`
`filter_sub` 📖	mathematical	—	`filter` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Finsupp` `instSub`	—	`AddMonoidHom.map_sub`
`filter_sum` 📖	mathematical	—	`filter` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finset.sum` `Finsupp` `instAddCommMonoid`	—	`map_sum` `AddMonoidHom.instAddMonoidHomClass`
`filter_zero` 📖	mathematical	—	`filter` `Finsupp` `instZero`	—	`support_eq_empty` `support_filter` `support_zero` `Finset.filter_empty`
`finite_range` 📖	mathematical	—	`Set.Finite` `Set.range` `DFunLike.coe` `Finsupp` `instFunLike`	—	`Set.Finite.subset` `range_subset_insert_frange`
`frange_single` 📖	mathematical	—	`Finset` `Finset.instHasSubset` `frange` `single` `Finset.instSingleton`	—	—
`fst_sumFinsuppAddEquivProdFinsupp` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instFunLike` `AddEquiv` `instAdd` `Prod.instAdd` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `sumFinsuppAddEquivProdFinsupp`	—	—
`fst_sumFinsuppEquivProdFinsupp` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `instFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `sumFinsuppEquivProdFinsupp`	—	—
`graph_eq_empty` 📖	mathematical	—	`graph` `Finset` `Finset.instEmptyCollection` `Finsupp` `instZero`	—	`graph_injective` `graph_zero`
`graph_inj` 📖	mathematical	—	`graph`	—	`graph_injective`
`graph_injective` 📖	mathematical	—	`Finsupp` `Finset` `graph`	—	`image_fst_graph` `ext_iff'` `apply_eq_of_mem_graph` `mk_mem_graph`
`graph_zero` 📖	mathematical	—	`graph` `Finsupp` `instZero` `Finset` `Finset.instEmptyCollection`	—	—
`image_fst_graph` 📖	mathematical	—	`Finset.image` `graph` `support`	—	`Finset.map_eq_image` `Finset.image_image` `Finset.image_id'`
`mapDomainEmbedding_apply` 📖	mathematical	—	`DFunLike.coe` `Function.Embedding` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Function.instFunLikeEmbedding` `mapDomainEmbedding` `mapDomain` `Nat.instAddCommMonoid`	—	—
`mapDomain_add` 📖	mathematical	—	`mapDomain` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAdd`	—	`sum_add_index'` `single_zero` `single_add`
`mapDomain_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instFunLike` `mapDomain`	—	`mapDomain.eq_1` `sum_apply` `sum_eq_single` `single_eq_of_ne'` `single_zero` `coe_zero` `Pi.zero_apply` `single_eq_same`
`mapDomain_apply'` 📖	mathematical	`Set` `Set.instHasSubset` `SetLike.coe` `Finset` `Finset.instSetLike` `support` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Set.InjOn` `Set.instMembership`	`DFunLike.coe` `Finsupp` `instFunLike` `mapDomain`	—	`mapDomain.eq_1` `sum_apply` `sum.eq_1` `Finset.sum_congr` `single_apply` `Finset.add_sum_erase` `Finset.sum_eq_zero` `Set.InjOn.ne` `Set.InjOn.mono` `Finset.mem_of_mem_erase` `Finset.ne_of_mem_erase` `add_zero` `notMem_support_iff`
`mapDomain_comapDomain` 📖	mathematical	`Set` `Set.instHasSubset` `SetLike.coe` `Finset` `Finset.instSetLike` `support` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Set.range`	`mapDomain` `comapDomain` `Function.Injective.injOn` `Set.preimage`	—	`Function.Injective.injOn` `Function.Embedding.injective` `embDomain_comapDomain` `embDomain_eq_mapDomain`
`mapDomain_comapDomain_nat_add_one` 📖	mathematical	—	`mapDomain` `DFunLike.coe` `AddMonoidHom` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddZeroClass` `AddMonoidHom.instFunLike` `comapDomain.addMonoidHom` `add_left_injective` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `erase`	—	`add_left_injective` `AddRightCancelSemigroup.toIsRightCancelAdd` `Function.Injective.injOn` `ext` `erase_ne` `mapDomain_comapDomain` `support_erase` `Finset.coe_erase`
`mapDomain_comp` 📖	mathematical	—	`mapDomain`	—	`sum_sum_index` `single_zero` `single_add` `sum_congr` `sum_single_index`
`mapDomain_congr` 📖	mathematical	—	`mapDomain`	—	`Finset.sum_congr`
`mapDomain_equiv_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instFunLike` `mapDomain` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm`	—	`Equiv.apply_symm_apply` `mapDomain_apply` `Equiv.injective`
`mapDomain_finset_sum` 📖	mathematical	—	`mapDomain` `Finset.sum` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoid`	—	`map_sum` `AddMonoidHom.instAddMonoidHomClass`
`mapDomain_id` 📖	mathematical	—	`mapDomain`	—	`sum_single`
`mapDomain_injOn` 📖	mathematical	`Set.InjOn`	`Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `mapDomain` `setOf` `Set` `Set.instHasSubset` `SetLike.coe` `Finset` `Finset.instSetLike` `support`	—	`ext` `mapDomain_apply'` `Set.union_subset`
`mapDomain_injective` 📖	mathematical	—	`Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `mapDomain`	—	`ext` `mapDomain_apply`
`mapDomain_mapRange` 📖	mathematical	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	`mapDomain` `mapRange`	—	`DFunLike.congr_fun` `mapDomain.addMonoidHom_comp_mapRange`
`mapDomain_notin_range` 📖	mathematical	`Set` `Set.instMembership` `Set.range`	`DFunLike.coe` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instFunLike` `mapDomain`	—	`mapDomain.eq_1` `sum_apply` `sum.eq_1` `Finset.sum_eq_zero` `single_eq_of_ne` `Set.mem_range_self`
`mapDomain_single` 📖	mathematical	—	`mapDomain` `single` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`sum_single_index` `single_zero`
`mapDomain_sum` 📖	mathematical	—	`mapDomain` `sum` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoid`	—	`map_finsuppSum` `AddMonoidHom.instAddMonoidHomClass`
`mapDomain_support` 📖	mathematical	—	`Finset` `Finset.instHasSubset` `support` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `mapDomain` `Finset.image`	—	`Finset.Subset.trans` `support_sum` `Finset.biUnion_mono` `support_single_subset` `Finset.biUnion_singleton` `subset_refl` `Finset.instReflSubset`
`mapDomain_support_of_injOn` 📖	mathematical	`Set.InjOn` `SetLike.coe` `Finset` `Finset.instSetLike` `support` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`mapDomain` `Finset.image`	—	`Finset.Subset.antisymm` `mapDomain_support` `mapDomain_apply'` `Finset.Subset.refl`
`mapDomain_support_of_injective` 📖	mathematical	—	`support` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `mapDomain` `Finset.image`	—	`mapDomain_support_of_injOn` `Function.Injective.injOn`
`mapDomain_surjective` 📖	mathematical	—	`Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `mapDomain`	—	`mapDomain_comp` `Function.rightInverse_surjInv` `mapDomain_id`
`mapDomain_zero` 📖	mathematical	—	`mapDomain` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instZero`	—	`sum_zero_index`
`mapRange_finset_sum` 📖	mathematical	—	`mapRange` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFunLike.coe` `map_zero` `AddMonoidHomClass.toZeroHomClass` `Finset.sum` `Finsupp` `instAddCommMonoid`	—	`map_sum` `AddMonoidHom.instAddMonoidHomClass`
`mapRange_multiset_sum` 📖	mathematical	—	`mapRange` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFunLike.coe` `map_zero` `AddMonoidHomClass.toZeroHomClass` `Multiset.sum` `Finsupp` `instAddCommMonoid` `Multiset.map`	—	`AddMonoidHom.map_multiset_sum`
`mem_frange` 📖	mathematical	—	`Finset` `Finset.instMembership` `frange` `Set` `Set.instMembership` `Set.range` `DFunLike.coe` `Finsupp` `instFunLike`	—	`frange.eq_1` `Finset.mem_image` `mem_support_iff`
`mem_frange_of_mem` 📖	mathematical	`Finset` `Finset.instMembership` `support`	`frange` `DFunLike.coe` `Finsupp` `instFunLike`	—	—
`mem_graph_iff` 📖	mathematical	—	`Finset` `Finset.instMembership` `graph` `DFunLike.coe` `Finsupp` `instFunLike`	—	`mk_mem_graph_iff`
`mem_range_mapDomain_iff` 📖	mathematical	—	`Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Set` `Set.instMembership` `Set.range` `mapDomain` `DFunLike.coe` `instFunLike`	—	`mapDomain_notin_range` `Function.Injective.injOn` `mapDomain_comapDomain`
`mem_splitSupport_iff_nonzero` 📖	mathematical	—	`Finset` `Finset.instMembership` `splitSupport`	—	`splitSupport.eq_1` `Finset.mem_image` `support_eq_empty` `Finset.nonempty_iff_ne_empty` `split.eq_1` `comapDomain.eq_1` `Finset.Nonempty.eq_1`
`mem_support_finset_sum` 📖	—	`Finset` `Finset.instMembership` `support` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finset.sum` `Finsupp` `instAddCommMonoid`	—	—	`mem_support_multiset_sum` `Multiset.mem_map`
`mem_support_multiset_sum` 📖	mathematical	`Finset` `Finset.instMembership` `support` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Multiset.sum` `Finsupp` `instAddCommMonoid`	`Multiset` `Multiset.instMembership`	—	`Multiset.induction_on` `Multiset.mem_cons_self` `mem_support_iff` `zero_add` `notMem_support_iff` `Multiset.sum_cons` `Multiset.mem_cons_of_mem`
`mk_mem_graph` 📖	mathematical	`Finset` `Finset.instMembership` `support`	`graph` `DFunLike.coe` `Finsupp` `instFunLike`	—	`mk_mem_graph_iff` `mem_support_iff`
`mk_mem_graph_iff` 📖	mathematical	—	`Finset` `Finset.instMembership` `graph` `DFunLike.coe` `Finsupp` `instFunLike`	—	—
`notMem_graph_snd_zero` 📖	mathematical	—	`Finset` `Finset.instMembership` `graph`	—	`mem_graph_iff`
`piecewise_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `instFunLike` `piecewise`	—	—
`piecewise_support` 📖	mathematical	—	`support` `piecewise` `Finset.disjUnion` `Finset.map` `Function.Embedding.subtype`	—	—
`prod_div_prod_filter` 📖	mathematical	—	`DivInvMonoid.toDiv` `Group.toDivInvMonoid` `CommGroup.toGroup` `prod` `CommGroup.toCommMonoid` `filter`	—	`div_eq_of_eq_mul'` `prod_filter_mul_prod_filter_not`
`prod_equivMapDomain` 📖	mathematical	—	`prod` `equivMapDomain` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`Finset.prod_congr` `Finset.prod_map` `Equiv.symm_apply_apply`
`prod_filter_index` 📖	mathematical	—	`prod` `filter` `Finset.prod` `support` `DFunLike.coe` `Finsupp` `instFunLike`	—	`Finset.prod_congr` `filter_apply_pos` `Finset.mem_filter` `support_filter`
`prod_filter_mul_prod_filter_not` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `prod` `filter`	—	`prod_filter_index` `Finset.prod_filter_mul_prod_filter_not`
`prod_mapDomain_index` 📖	mathematical	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `MulOne.toMul`	`prod` `mapDomain`	—	`prod_sum_index` `prod_congr` `prod_single_index`
`prod_mapDomain_index_inj` 📖	mathematical	—	`prod` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `mapDomain`	—	`embDomain_eq_mapDomain` `prod_embDomain`
`prod_subtypeDomain_index` 📖	mathematical	—	`prod` `subtypeDomain`	—	`Finset.prod_bij`
`prod_sumElim` 📖	mathematical	—	`prod` `sumElim` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid`	—	`Finset.prod_congr` `Finset.prod_disjSum`
`range_subset_insert_frange` 📖	mathematical	—	`Set` `Set.instHasSubset` `Set.range` `DFunLike.coe` `Finsupp` `instFunLike` `Set.instInsert` `SetLike.coe` `Finset` `Finset.instSetLike` `frange`	—	—
`restrictSupportEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Set` `Set.instHasSubset` `SetLike.coe` `Finset` `Finset.instSetLike` `support` `Set.Elem` `EquivLike.toFunLike` `Equiv.instEquivLike` `restrictSupportEquiv` `subtypeDomain` `Set.instMembership`	—	—
`restrictSupportEquiv_symm_apply_coe` 📖	mathematical	—	`Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Set` `Set.instHasSubset` `SetLike.coe` `Finset` `Finset.instSetLike` `support` `DFunLike.coe` `Equiv` `Set.Elem` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `restrictSupportEquiv` `extendDomain` `Set.instMembership`	—	`restrictSupportEquiv.eq_1`
`restrictSupportEquiv_symm_single` 📖	mathematical	—	`Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Set` `Set.instHasSubset` `SetLike.coe` `Finset` `Finset.instSetLike` `support` `DFunLike.coe` `Equiv` `Set.Elem` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `restrictSupportEquiv` `single` `Set.instMembership`	—	`restrictSupportEquiv_symm_apply_coe` `extendDomain_single`
`sigmaFinsuppAddEquivPiFinsupp_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instFunLike` `AddEquiv` `instAdd` `Pi.instAdd` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `sigmaFinsuppAddEquivPiFinsupp`	—	—
`sigmaFinsuppEquivPiFinsupp_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `instFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `sigmaFinsuppEquivPiFinsupp`	—	—
`sigma_sum` 📖	mathematical	—	`sum` `Finset.sum` `splitSupport` `split`	—	`Finset.sum_congr` `sigma_support` `Finset.sum_sigma` `split_apply`
`sigma_support` 📖	mathematical	—	`support` `Finset.sigma` `splitSupport` `split`	—	—
`snd_sumFinsuppAddEquivProdFinsupp` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instFunLike` `AddEquiv` `instAdd` `Prod.instAdd` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `sumFinsuppAddEquivProdFinsupp`	—	—
`snd_sumFinsuppEquivProdFinsupp` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `instFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `sumFinsuppEquivProdFinsupp`	—	—
`split_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `instFunLike` `split`	—	`split.eq_1` `comapDomain_apply`
`subtypeDomain_add` 📖	mathematical	—	`subtypeDomain` `AddZero.toZero` `AddZeroClass.toAddZero` `Finsupp` `instAdd`	—	`ext`
`subtypeDomain_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `instFunLike` `subtypeDomain`	—	—
`subtypeDomain_eq_iff` 📖	mathematical	—	`subtypeDomain`	—	`subtypeDomain_eq_iff_forall` `ext` `em` `notMem_support_iff`
`subtypeDomain_eq_iff_forall` 📖	mathematical	—	`subtypeDomain` `DFunLike.coe` `Finsupp` `instFunLike`	—	—
`subtypeDomain_eq_zero_iff` 📖	mathematical	—	`subtypeDomain` `Finsupp` `instZero`	—	`subtypeDomain_eq_iff` `instIsEmptyFalse`
`subtypeDomain_eq_zero_iff'` 📖	mathematical	—	`subtypeDomain` `Finsupp` `instZero` `DFunLike.coe` `instFunLike`	—	`subtypeDomain_eq_iff_forall`
`subtypeDomain_extendDomain` 📖	mathematical	—	`subtypeDomain` `extendDomain`	—	`subtypeDomain_piecewise`
`subtypeDomain_finsupp_sum` 📖	mathematical	—	`subtypeDomain` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `sum` `Finsupp` `instAddCommMonoid`	—	`subtypeDomain_sum`
`subtypeDomain_neg` 📖	mathematical	—	`subtypeDomain` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Finsupp` `instNeg`	—	`ext`
`subtypeDomain_not_piecewise` 📖	mathematical	—	`subtypeDomain` `piecewise`	—	`ext` `Subtype.prop`
`subtypeDomain_piecewise` 📖	mathematical	—	`subtypeDomain` `piecewise`	—	`ext` `Subtype.prop`
`subtypeDomain_sub` 📖	mathematical	—	`subtypeDomain` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Finsupp` `instSub`	—	`ext`
`subtypeDomain_sum` 📖	mathematical	—	`subtypeDomain` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finset.sum` `Finsupp` `instAddCommMonoid`	—	`map_sum` `AddMonoidHom.instAddMonoidHomClass`
`subtypeDomain_zero` 📖	mathematical	—	`subtypeDomain` `Finsupp` `instZero`	—	—
`sumElim_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `instFunLike` `sumElim`	—	—
`sumElim_inl` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `instFunLike` `sumElim`	—	—
`sumElim_inr` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `instFunLike` `sumElim`	—	—
`sumElim_support` 📖	mathematical	—	`support` `sumElim` `Finset.disjSum`	—	—
`sumFinsuppAddEquivProdFinsupp_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instAdd` `Prod.instAdd` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `sumFinsuppAddEquivProdFinsupp` `comapDomain`	—	—
`sumFinsuppAddEquivProdFinsupp_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Prod.instAdd` `instAdd` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `sumFinsuppAddEquivProdFinsupp` `sumElim`	—	—
`sumFinsuppAddEquivProdFinsupp_symm_inl` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instFunLike` `AddEquiv` `Prod.instAdd` `instAdd` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `sumFinsuppAddEquivProdFinsupp`	—	—
`sumFinsuppAddEquivProdFinsupp_symm_inr` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instFunLike` `AddEquiv` `Prod.instAdd` `instAdd` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `sumFinsuppAddEquivProdFinsupp`	—	—
`sumFinsuppEquivProdFinsupp_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Finsupp` `EquivLike.toFunLike` `Equiv.instEquivLike` `sumFinsuppEquivProdFinsupp` `comapDomain`	—	—
`sumFinsuppEquivProdFinsupp_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Finsupp` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `sumFinsuppEquivProdFinsupp` `sumElim`	—	—
`sumFinsuppEquivProdFinsupp_symm_inl` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `instFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `sumFinsuppEquivProdFinsupp`	—	—
`sumFinsuppEquivProdFinsupp_symm_inr` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `instFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `sumFinsuppEquivProdFinsupp`	—	—
`sum_comapDomain` 📖	mathematical	`Set.BijOn` `Set.preimage` `SetLike.coe` `Finset` `Finset.instSetLike` `support`	`sum` `comapDomain` `Set.BijOn.injOn`	—	`Finset.sum_preimage_of_bij`
`sum_curry_index` 📖	mathematical	—	`sum` `Finsupp` `instZero` `curry`	—	`sum_uncurry_index'` `uncurry_curry`
`sum_equivMapDomain` 📖	mathematical	—	`sum` `equivMapDomain` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`Finset.sum_congr` `Finset.sum_map` `Equiv.symm_apply_apply`
`sum_filter_add_sum_filter_not` 📖	mathematical	—	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `sum` `filter`	—	`sum_filter_index` `Finset.sum_filter_add_sum_filter_not`
`sum_filter_index` 📖	mathematical	—	`sum` `filter` `Finset.sum` `support` `DFunLike.coe` `Finsupp` `instFunLike`	—	`Finset.sum_congr` `filter_apply_pos` `Finset.mem_filter` `support_filter`
`sum_mapDomain_index` 📖	mathematical	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddZero.toAdd`	`sum` `mapDomain`	—	`sum_sum_index` `sum_congr` `sum_single_index`
`sum_mapDomain_index_addMonoidHom` 📖	mathematical	—	`sum` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `mapDomain` `DFunLike.coe` `AddMonoidHom` `AddMonoidHom.instFunLike`	—	`sum_mapDomain_index` `AddMonoidHom.map_zero` `AddMonoidHom.map_add`
`sum_mapDomain_index_inj` 📖	mathematical	—	`sum` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `mapDomain`	—	`embDomain_eq_mapDomain` `sum_embDomain`
`sum_sub_sum_filter` 📖	mathematical	—	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `sum` `AddCommGroup.toAddCommMonoid` `filter`	—	`sub_eq_of_eq_add'` `sum_filter_add_sum_filter_not`
`sum_subtypeDomain_index` 📖	mathematical	—	`sum` `subtypeDomain`	—	`Finset.sum_bij` `mem_support_iff`
`sum_sumElim` 📖	mathematical	—	`sum` `sumElim` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`Finset.sum_congr` `Finset.sum_disjSum`
`sum_uncurry_index` 📖	mathematical	—	`sum` `uncurry` `Finsupp` `instZero`	—	`Finset.sum_congr` `Finset.sum_disjiUnion` `Finset.sum_map`
`sum_uncurry_index'` 📖	mathematical	—	`sum` `uncurry` `Finsupp` `instZero`	—	`sum_uncurry_index`
`sum_update_add` 📖	mathematical	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddZero.toAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	`sum` `update` `DFunLike.coe` `Finsupp` `instFunLike`	—	`update_eq_erase_add_single` `sum_add_index'` `update_self` `add_assoc` `add_comm` `sum_single_index`
`support_curry` 📖	mathematical	—	`support` `Finsupp` `instZero` `curry` `Finset.image`	—	`Lean.Meta.FastSubsingleton.elim` `Lean.Meta.instFastSubsingletonForall` `Lean.Meta.instFastSubsingletonDecidable`
`support_extendDomain_subset` 📖	mathematical	—	`Set` `Set.instHasSubset` `SetLike.coe` `Finset` `Finset.instSetLike` `support` `extendDomain` `setOf`	—	—
`support_filter` 📖	mathematical	—	`support` `filter` `Finset.filter`	—	—
`support_subtypeDomain` 📖	mathematical	—	`support` `subtypeDomain` `Finset.subtype`	—	—
`uncurry_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `instFunLike` `uncurry` `instZero`	—	—
`uncurry_apply_pair` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `instFunLike` `uncurry` `instZero`	—	—
`uncurry_curry` 📖	mathematical	—	`uncurry` `curry`	—	`ext`
`uncurry_single` 📖	mathematical	—	`uncurry` `single` `Finsupp` `instZero`	—	`ext` `eq_or_ne` `single_eq_same` `single_apply` `single_eq_of_ne'`
`zero_notMem_frange` 📖	mathematical	—	`Finset` `Finset.instMembership` `frange`	—	`mem_frange`

Finsupp.comapDomain

Definitions

Name	Category	Theorems
`addMonoidHom` 📖	CompOp	3 math math: `Finsupp.mapDomain_comapDomain_nat_add_one`, `LinearMap.snd_prodOfFinsuppNat`, `addMonoidHom_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addMonoidHom_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `Finsupp.instAddZeroClass` `AddMonoidHom.instFunLike` `addMonoidHom` `Finsupp.comapDomain`	—	—

Finsupp.mapDomain

Definitions

Name	Category	Theorems
`addMonoidHom` 📖	CompOp	5 math math: `addMonoidHom_comp`, `AddCommMonCat.free_map`, `addMonoidHom_apply`, `addMonoidHom_id`, `addMonoidHom_comp_mapRange`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addMonoidHom_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finsupp.instAddZeroClass` `AddMonoidHom.instFunLike` `addMonoidHom` `Finsupp.mapDomain`	—	—
`addMonoidHom_comp` 📖	mathematical	—	`addMonoidHom` `AddMonoidHom.comp` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finsupp.instAddZeroClass`	—	`AddMonoidHom.ext` `Finsupp.mapDomain_comp`
`addMonoidHom_comp_mapRange` 📖	mathematical	—	`AddMonoidHom.comp` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finsupp.instAddZeroClass` `addMonoidHom` `Finsupp.mapRange.addMonoidHom`	—	`Finsupp.addHom_ext'` `AddMonoidHom.ext` `Finsupp.ext` `Finsupp.mapRange_single` `Finsupp.mapDomain_single`
`addMonoidHom_id` 📖	mathematical	—	`addMonoidHom` `AddMonoidHom.id` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finsupp.instAddZeroClass`	—	`AddMonoidHom.ext` `Finsupp.mapDomain_id`

Int

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cast_finsuppProd` 📖	mathematical	—	`AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `CommRing.toRing` `Finsupp.prod` `instCommMonoid` `CommRing.toCommMonoid`	—	`cast_prod`
`cast_finsupp_sum` 📖	mathematical	—	`AddGroupWithOne.toIntCast` `AddCommGroupWithOne.toAddGroupWithOne` `Finsupp.sum` `instAddCommMonoid` `AddCommMonoidWithOne.toAddCommMonoid` `AddCommGroupWithOne.toAddCommMonoidWithOne`	—	`cast_sum`

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cast_finsuppProd` 📖	mathematical	—	`AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Finsupp.prod` `instCommMonoid` `CommSemiring.toCommMonoid`	—	`cast_prod`
`cast_finsupp_sum` 📖	mathematical	—	`AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `Finsupp.sum` `instAddCommMonoid` `AddCommMonoidWithOne.toAddCommMonoid`	—	`cast_sum`

Rat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cast_finsuppProd` 📖	mathematical	—	`DivisionRing.toRatCast` `Field.toDivisionRing` `Finsupp.prod` `commMonoid` `CommRing.toCommMonoid` `Field.toCommRing`	—	`cast_prod`
`cast_finsupp_sum` 📖	mathematical	—	`DivisionRing.toRatCast` `Finsupp.sum` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `DivisionRing.toRing`	—	`cast_sum`

---

← Back to Index