BigOperators

📁 Source: Mathlib/Data/DFinsupp/BigOperators.lean

Statistics

Metric	Count
Definitions `evalAddMonoidHom`, `liftAddHom`, `prod`, `sum`, `sumAddHom`, `sumZeroHom`	6
Theorems `map_dfinsuppSumAddHom`, `coe_dfinsuppSum`, `coe_dfinsuppSumAddHom`, `dfinsuppSumAddHom_apply`, `dfinsuppSum_apply`, `map_dfinsuppSumAddHom`, `coe_finset_sum`, `comp_liftAddHom`, `comp_sumAddHom`, `finset_sum_apply`, `liftAddHom_apply`, `liftAddHom_apply_single`, `liftAddHom_comp_single`, `liftAddHom_singleAddHom`, `liftAddHom_symm_apply`, `prod_add_index`, `prod_comm`, `prod_eq_one`, `prod_eq_prod_fintype`, `prod_eq_zero_iff`, `prod_finset_sum_index`, `prod_inv`, `prod_mapRange_index`, `prod_mul`, `prod_ne_zero_iff`, `prod_neg_index`, `prod_one`, `prod_single_index`, `prod_subtypeDomain_index`, `prod_sum_index`, `prod_zero_index`, `smul_sum`, `subtypeDomain_finsupp_sum`, `subtypeDomain_sum`, `sumAddHom_add`, `sumAddHom_apply`, `sumAddHom_comm`, `sumAddHom_comp_single`, `sumAddHom_piSingle`, `sumAddHom_single`, `sumAddHom_singleAddHom`, `sumAddHom_toZeroHom`, `sumAddHom_zero`, `sumZeroHom_apply`, `sumZeroHom_piSingle`, `sumZeroHom_single`, `sum_add`, `sum_add_index`, `sum_apply`, `sum_comm`, `sum_eq_sum_fintype`, `sum_eq_zero`, `sum_finset_sum_index`, `sum_mapRange_index`, `sum_neg`, `sum_neg_index`, `sum_single`, `sum_single_index`, `sum_sub_index`, `sum_subtypeDomain_index`, `sum_sum_index`, `sum_zero`, `sum_zero_index`, `support_sum`, `coe_dfinsuppProd`, `dfinsuppProd_apply`, `map_dfinsuppSumAddHom`, `map_dfinsuppProd`, `map_dfinsuppSum`	69
Total	75

AddEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_dfinsuppSumAddHom` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `EquivLike.toFunLike` `instEquivLike` `AddMonoidHom` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `DFinsupp.addZeroClass` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddMonoidHom.instFunLike` `DFinsupp.sumAddHom` `AddMonoidHom.comp` `toAddMonoidHom`	—	`DFunLike.congr_fun` `DFinsupp.comp_liftAddHom`

AddMonoidHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_dfinsuppSum` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instFunLike` `DFinsupp.sum` `instAddCommMonoid` `Pi.addCommMonoid`	—	`coe_finset_sum`
`coe_dfinsuppSumAddHom` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instFunLike` `DFinsupp` `AddZero.toZero` `DFinsupp.addZeroClass` `instAddCommMonoid` `DFinsupp.sumAddHom` `Pi.addCommMonoid` `comp` `Pi.addZeroClass` `coeFn`	—	`map_dfinsuppSumAddHom`
`dfinsuppSumAddHom_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instFunLike` `DFinsupp` `AddZero.toZero` `DFinsupp.addZeroClass` `instAddCommMonoid` `DFinsupp.sumAddHom` `comp` `eval`	—	`map_dfinsuppSumAddHom`
`dfinsuppSum_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instFunLike` `DFinsupp.sum` `instAddCommMonoid`	—	`finset_sum_apply`
`map_dfinsuppSumAddHom` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instFunLike` `DFinsupp` `AddZero.toZero` `DFinsupp.addZeroClass` `DFinsupp.sumAddHom` `comp`	—	`DFunLike.congr_fun` `DFinsupp.comp_liftAddHom`

DFinsupp

Definitions

Name	Category	Theorems
`evalAddMonoidHom` 📖	CompOp	1 math math: `sumAddHom_piSingle`
`liftAddHom` 📖	CompOp	6 math math: `liftAddHom_apply`, `liftAddHom_apply_single`, `comp_liftAddHom`, `liftAddHom_singleAddHom`, `liftAddHom_comp_single`, `liftAddHom_symm_apply`
`prod` 📖	CompOp	20 math math: `prod_single_index`, `prod_mul`, `prod_add_index`, `prod_eq_zero_iff`, `prod_sum_index`, `prod_eq_prod_fintype`, `prod_neg_index`, `prod_eq_one`, `prod_finset_sum_index`, `card_pi`, `prod_zero_index`, `prod_one`, `MonoidHom.coe_dfinsuppProd`, `prod_subtypeDomain_index`, `dfinsuppProd_mem`, `map_dfinsuppProd`, `prod_mapRange_index`, `MonoidHom.dfinsuppProd_apply`, `prod_inv`, `prod_comm`
`sum` 📖	CompOp	45 math math: `coprodMap_apply`, `MvPolynomial.DirectSum.coeLinearMap_eq_dfinsuppSum`, `sum_zero_index`, `DirectSum.coeAddMonoidHom_eq_dfinsuppSum`, `sum_add`, `OrthogonalFamily.linearIsometry_apply_dfinsupp_sum_single`, `sum_sum_index`, `LinearMap.dfinsuppSum_apply`, `sum_zero`, `DirectSum.coeLinearMap_eq_dfinsuppSum`, `sumZeroHom_apply`, `sum_eq_sum_fintype`, `prod_sum_index`, `sum_subtypeDomain_index`, `MvPolynomial.DirectSum.coeAddMonoidHom_eq_support_sum`, `sum_apply`, `LinearMap.coe_dfinsuppSum`, `map_dfinsuppSum`, `AddMonoidHom.dfinsuppSum_apply`, `subtypeDomain_finsupp_sum`, `sum_neg`, `Submodule.dfinsuppSum_mem`, `sum_finset_sum_index`, `sum_comm`, `IsHilbertSum.linearIsometryEquiv_symm_apply_dfinsupp_sum_single`, `sum_neg_index`, `sumAddHom_apply`, `sum_eq_zero`, `DirectSum.mul_eq_dfinsuppSum`, `DirectSum.coe_mul_apply_eq_dfinsuppSum`, `AddSubmonoid.mem_iSup_iff_exists_dfinsupp'`, `sum_mapRange_index`, `sum_single_index`, `AddMonoidHom.coe_dfinsuppSum`, `sum_sub_index`, `dfinsuppSum_mem`, `inner_sum`, `Submodule.mem_iSup_iff_exists_dfinsupp'`, `support_sum`, `IsHilbertSum.linearIsometryEquiv_apply_dfinsupp_sum_single`, `smul_sum`, `sum_inner`, `sum_add_index`, `OrthogonalFamily.inner_right_dfinsupp`, `sum_single`
`sumAddHom` 📖	CompOp	28 math math: `liftAddHom_apply`, `AddMonoidHom.map_dfinsuppSumAddHom`, `iSupIndep.dfinsuppSumAddHom_injective`, `sumAddHom_single`, `AddMonoidHom.coe_dfinsuppSumAddHom`, `AddEquiv.map_dfinsuppSumAddHom`, `sumAddHom_comm`, `LinearMap.map_dfinsuppSumAddHom`, `AddSubmonoid.mem_bsupr_iff_exists_dfinsupp`, `AddSubmonoid.iSup_eq_mrange_dfinsuppSumAddHom`, `sumAddHom_piSingle`, `iSupIndep.linearEquiv_apply`, `LinearEquiv.map_dfinsuppSumAddHom`, `AddSubmonoid.bsupr_eq_mrange_dfinsuppSumAddHom`, `sumAddHom_apply`, `sumAddHom_comp_single`, `sumAddHom_zero`, `sumAddHom_singleAddHom`, `AddSubmonoid.mem_iSup_iff_exists_dfinsupp`, `dfinsuppSumAddHom_mem`, `comp_sumAddHom`, `sumAddHom_add`, `AddMonoidHom.dfinsuppSumAddHom_apply`, `RingHom.map_dfinsuppSumAddHom`, `Submodule.dfinsuppSumAddHom_mem`, `lsum_apply_apply`, `iSupIndep_iff_dfinsuppSumAddHom_injective`, `sumAddHom_toZeroHom`
`sumZeroHom` 📖	CompOp	4 math math: `sumZeroHom_apply`, `sumZeroHom_piSingle`, `sumZeroHom_single`, `sumAddHom_toZeroHom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_finset_sum` 📖	mathematical	—	`DFunLike.coe` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instDFunLike` `Finset.sum` `addCommMonoid` `Pi.addCommMonoid`	—	`map_sum` `AddMonoidHom.instAddMonoidHomClass`
`comp_liftAddHom` 📖	mathematical	—	`AddMonoidHom.comp` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `addZeroClass` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFunLike.coe` `AddEquiv` `AddMonoidHom` `Pi.instAdd` `AddMonoidHom.add` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `liftAddHom`	—	`AddEquiv.symm_apply_eq` `liftAddHom_symm_apply` `AddMonoidHom.comp_assoc` `liftAddHom_comp_single`
`comp_sumAddHom` 📖	mathematical	—	`AddMonoidHom.comp` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `addZeroClass` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `sumAddHom`	—	`comp_liftAddHom`
`finset_sum_apply` 📖	mathematical	—	`DFunLike.coe` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instDFunLike` `Finset.sum` `addCommMonoid`	—	`map_sum` `AddMonoidHom.instAddMonoidHomClass`
`liftAddHom_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `AddMonoidHom` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `addZeroClass` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Pi.instAdd` `AddMonoidHom.add` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `liftAddHom` `sumAddHom`	—	—
`liftAddHom_apply_single` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `addZeroClass` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddMonoidHom.instFunLike` `AddEquiv` `Pi.instAdd` `AddMonoidHom.add` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `liftAddHom` `single`	—	`sumAddHom_single`
`liftAddHom_comp_single` 📖	mathematical	—	`AddMonoidHom.comp` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `addZeroClass` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFunLike.coe` `AddEquiv` `AddMonoidHom` `Pi.instAdd` `AddMonoidHom.add` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `liftAddHom` `singleAddHom`	—	`sumAddHom_comp_single`
`liftAddHom_singleAddHom` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `AddMonoidHom` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addZeroClass` `addCommMonoid` `Pi.instAdd` `AddMonoidHom.add` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `liftAddHom` `singleAddHom` `AddMonoidHom.id`	—	`Equiv.apply_eq_iff_eq_symm_apply`
`liftAddHom_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `AddMonoidHom` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `addZeroClass` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddMonoidHom.add` `Pi.instAdd` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `liftAddHom` `AddMonoidHom.comp` `singleAddHom`	—	—
`prod_add_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` `DFinsupp` `instAdd`	—	`Finset.prod_subset` `Finset.subset_union_left` `Finset.subset_union_right` `support_add` `Finset.prod_congr` `Finset.prod_mul_distrib`
`prod_comm` 📖	mathematical	—	`prod`	—	`Finset.prod_comm`
`prod_eq_one` 📖	mathematical	`DFunLike.coe` `DFinsupp` `instDFunLike` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid`	`prod`	—	`Finset.prod_eq_one`
`prod_eq_prod_fintype` 📖	mathematical	`MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid`	`prod` `Finset.prod` `Finset.univ` `DFunLike.coe` `Equiv` `DFinsupp` `EquivLike.toFunLike` `Equiv.instEquivLike` `equivFunOnFintype`	—	`Finset.prod_subset` `Finset.subset_univ` `mem_support_iff` `Finset.prod_congr`
`prod_eq_zero_iff` 📖	mathematical	—	`prod` `CommMonoidWithZero.toCommMonoid` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `Finset` `Finset.instMembership` `support` `DFunLike.coe` `DFinsupp` `instDFunLike`	—	`Finset.prod_eq_zero_iff`
`prod_finset_sum_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`	`Finset.prod` `prod` `Finset.sum` `DFinsupp` `addCommMonoid`	—	`Finset.induction_on` `Finset.prod_insert` `prod.congr_simp` `Finset.sum_insert` `prod_add_index`
`prod_inv` 📖	mathematical	—	`prod` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DivisionCommMonoid.toCommMonoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid`	—	`map_prod` `MonoidHom.instMonoidHomClass`
`prod_mapRange_index` 📖	mathematical	`MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid`	`prod` `mapRange`	—	`mapRange_def` `Finset.prod_subset` `support_mk_subset` `Finset.prod_congr`
`prod_mul` 📖	mathematical	—	`prod` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid`	—	`Finset.prod_mul_distrib`
`prod_ne_zero_iff` 📖	—	—	—	—	`Finset.prod_ne_zero_iff`
`prod_neg_index` 📖	mathematical	`NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid`	`prod` `DFinsupp` `instNeg` `NegZeroClass.toNeg`	—	`prod_mapRange_index`
`prod_one` 📖	mathematical	—	`prod` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid`	—	`Finset.prod_const_one`
`prod_single_index` 📖	mathematical	`MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid`	`prod` `single`	—	`Finset.prod_congr` `support_single_ne_zero` `single_apply` `Finset.prod_singleton` `prod.congr_simp` `single_zero`
`prod_subtypeDomain_index` 📖	mathematical	—	`prod` `subtypeDomain`	—	`Finset.prod_bij` `support_subtypeDomain`
`prod_sum_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` `sum` `DFinsupp` `addCommMonoid`	—	`prod_finset_sum_index`
`prod_zero_index` 📖	mathematical	—	`prod` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFinsupp` `instZero` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid`	—	—
`smul_sum` 📖	mathematical	—	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `sum`	—	`Finset.smul_sum`
`subtypeDomain_finsupp_sum` 📖	mathematical	—	`subtypeDomain` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `sum` `DFinsupp` `addCommMonoid`	—	`subtypeDomain_sum`
`subtypeDomain_sum` 📖	mathematical	—	`subtypeDomain` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finset.sum` `DFinsupp` `addCommMonoid`	—	`map_sum` `AddMonoidHom.instAddMonoidHomClass`
`sumAddHom_add` 📖	mathematical	—	`sumAddHom` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddMonoidHom.add` `DFinsupp` `AddZero.toZero` `addZeroClass`	—	`map_add` `AddMonoidHomClass.toAddHomClass` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass`
`sumAddHom_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `addZeroClass` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddMonoidHom.instFunLike` `sumAddHom` `sum`	—	`sumZeroHom_apply`
`sumAddHom_comm` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `addZeroClass` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddMonoidHom.instFunLike` `sumAddHom` `AddMonoidHom.instAddCommMonoid` `AddMonoidHom.flip`	—	`Finset.sum_congr` `AddMonoidHom.finset_sum_apply` `Finset.sum_comm`
`sumAddHom_comp_single` 📖	mathematical	—	`AddMonoidHom.comp` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `addZeroClass` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `sumAddHom` `singleAddHom`	—	`AddMonoidHom.ext` `sumAddHom_single`
`sumAddHom_piSingle` 📖	mathematical	—	`sumAddHom` `Pi.single` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instZeroAddMonoidHom` `AddMonoidHom.comp` `DFinsupp` `AddZero.toZero` `addZeroClass` `evalAddMonoidHom`	—	`AddMonoidHom.toZeroHom_injective` `sumAddHom_toZeroHom` `Pi.apply_single` `sumZeroHom_piSingle`
`sumAddHom_single` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `addZeroClass` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddMonoidHom.instFunLike` `sumAddHom` `single`	—	`sumZeroHom_single`
`sumAddHom_singleAddHom` 📖	mathematical	—	`sumAddHom` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addCommMonoid` `singleAddHom` `AddMonoidHom.id` `addZeroClass`	—	`liftAddHom_singleAddHom`
`sumAddHom_toZeroHom` 📖	mathematical	—	`AddMonoidHom.toZeroHom` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `addZeroClass` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `sumAddHom` `sumZeroHom`	—	—
`sumAddHom_zero` 📖	mathematical	—	`sumAddHom` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instZeroAddMonoidHom` `DFinsupp` `AddZero.toZero` `addZeroClass`	—	`map_zero` `AddMonoidHomClass.toZeroHomClass` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass`
`sumZeroHom_apply` 📖	mathematical	—	`DFunLike.coe` `ZeroHom` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `instZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `ZeroHom.funLike` `sumZeroHom` `sum`	—	`Finset.sum_filter` `Finset.sum_congr` `map_zero` `ZeroHom.zeroHomClass`
`sumZeroHom_piSingle` 📖	mathematical	—	`sumZeroHom` `Pi.single` `ZeroHom` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instZeroZeroHom` `ZeroHom.comp` `DFinsupp` `instZero` `DFunLike.coe` `instDFunLike`	—	`ZeroHom.ext` `Finset.sum_congr` `Finset.sum_eq_single` `Pi.single_eq_of_ne` `Pi.single_eq_same` `map_zero` `ZeroHom.zeroHomClass`
`sumZeroHom_single` 📖	mathematical	—	`DFunLike.coe` `ZeroHom` `DFinsupp` `instZero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `ZeroHom.funLike` `sumZeroHom` `single`	—	`Multiset.toFinset_singleton` `Finset.sum_singleton` `Pi.single_eq_same`
`sum_add` 📖	mathematical	—	`sum` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddZero.toAdd`	—	`Finset.sum_add_distrib`
`sum_add_index` 📖	mathematical	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddZero.toAdd`	`sum` `DFinsupp` `instAdd`	—	`Finset.sum_subset` `Finset.subset_union_left` `Finset.mem_union` `mem_support_toFun` `Finset.subset_union_right` `support_add` `Finset.sum_congr` `Finset.sum_add_distrib`
`sum_apply` 📖	mathematical	—	`DFunLike.coe` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instDFunLike` `sum` `addCommMonoid`	—	`map_sum` `AddMonoidHom.instAddMonoidHomClass`
`sum_comm` 📖	mathematical	—	`sum`	—	`Finset.sum_comm`
`sum_eq_sum_fintype` 📖	mathematical	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`sum` `Finset.sum` `Finset.univ` `DFunLike.coe` `Equiv` `DFinsupp` `EquivLike.toFunLike` `Equiv.instEquivLike` `equivFunOnFintype`	—	`Finset.sum_subset` `Finset.subset_univ` `mem_support_iff` `Finset.sum_congr`
`sum_eq_zero` 📖	mathematical	`DFunLike.coe` `DFinsupp` `instDFunLike` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`sum`	—	`Finset.sum_eq_zero`
`sum_finset_sum_index` 📖	mathematical	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddZero.toAdd`	`Finset.sum` `sum` `DFinsupp` `addCommMonoid`	—	`Finset.induction_on` `Finset.sum_insert` `sum.congr_simp` `sum_add_index`
`sum_mapRange_index` 📖	mathematical	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`sum` `mapRange`	—	`mapRange_def` `Finset.sum_subset` `support_mk_subset` `mem_support_toFun` `Finset.sum_congr`
`sum_neg` 📖	mathematical	—	`sum` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SubtractionCommMonoid.toAddCommMonoid` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid`	—	`map_sum` `AddMonoidHom.instAddMonoidHomClass`
`sum_neg_index` 📖	mathematical	`NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`sum` `DFinsupp` `instNeg` `NegZeroClass.toNeg`	—	`sum_mapRange_index`
`sum_single` 📖	mathematical	—	`sum` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addCommMonoid` `single`	—	`DFunLike.congr_fun` `liftAddHom_singleAddHom` `sumAddHom_apply` `liftAddHom_apply`
`sum_single_index` 📖	mathematical	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`sum` `single`	—	`Finset.sum_congr` `support_single_ne_zero` `single_apply` `Finset.sum_singleton` `sum.congr_simp` `single_zero`
`sum_sub_index` 📖	mathematical	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	`sum` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddCommGroup.toAddCommMonoid` `DFinsupp` `instSub`	—	`AddMonoidHom.map_sub` `sumAddHom_apply` `liftAddHom_apply`
`sum_subtypeDomain_index` 📖	mathematical	—	`sum` `subtypeDomain`	—	`Finset.sum_bij` `mem_support_toFun` `support_subtypeDomain` `Finset.mem_subtype`
`sum_sum_index` 📖	mathematical	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddZero.toAdd`	`sum` `DFinsupp` `addCommMonoid`	—	`sum_finset_sum_index`
`sum_zero` 📖	mathematical	—	`sum` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`Finset.sum_const_zero`
`sum_zero_index` 📖	mathematical	—	`sum` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFinsupp` `instZero`	—	—
`support_sum` 📖	mathematical	—	`Finset` `Finset.instHasSubset` `support` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `sum` `DFinsupp` `addCommMonoid` `Finset.biUnion` `DFunLike.coe` `instDFunLike`	—	`Finset.exists_ne_zero_of_sum_ne_zero` `mem_support_iff` `sum_apply`

MonoidHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_dfinsuppProd` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `instFunLike` `DFinsupp.prod` `instCommMonoid` `Pi.commMonoid`	—	`coe_finset_prod`
`dfinsuppProd_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `instFunLike` `DFinsupp.prod` `instCommMonoid`	—	`finset_prod_apply`

RingHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_dfinsuppSumAddHom` 📖	mathematical	—	`DFunLike.coe` `RingHom` `instFunLike` `AddMonoidHom` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `DFinsupp.addZeroClass` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `AddMonoidHom.instFunLike` `DFinsupp.sumAddHom` `AddMonoidHom.comp` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `toAddMonoidHom`	—	`DFunLike.congr_fun` `DFinsupp.comp_liftAddHom`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_dfinsuppProd` 📖	mathematical	—	`DFunLike.coe` `DFinsupp.prod`	—	`map_prod`
`map_dfinsuppSum` 📖	mathematical	—	`DFunLike.coe` `DFinsupp.sum`	—	`map_sum`

---

← Back to Index