Finset

📁 Source: Mathlib/Algebra/BigOperators/Ring/Finset.lean

Statistics

Metric	Count
Definitions	0
Theorems `sum_left`, `sum_right`, `dvd_sum`, `mul_sum`, `natCast_card_filter`, `prod_add`, `prod_add_one`, `prod_add_ordered`, `prod_add_prod_eq`, `prod_natCast`, `prod_neg`, `prod_one_add`, `prod_one_add_ordered`, `prod_one_sub_ordered`, `prod_range_natCast_sub`, `prod_sub`, `prod_sub_ordered`, `prod_sum`, `prod_univ_sum`, `sum_boole`, `sum_boole_mul`, `sum_mul`, `sum_mul_boole`, `sum_mul_sum`, `sum_pow'`, `sum_pow_mul_eq_add_pow`, `sum_prod_piFinset`, `sum_range_succ_mul_sum_range_succ`, `prod_add`, `prod_sum`, `sum_mul_sum`, `sum_pow`, `sum_pow_mul_eq_add_pow`, `cast_list_prod`, `cast_list_sum`, `cast_multiset_prod`, `cast_multiset_sum`, `cast_prod`, `cast_sum`, `sum_div`, `cast_list_prod`, `cast_list_sum`, `cast_multiset_prod`, `cast_multiset_sum`, `cast_prod`, `cast_sum`, `sum_div`	47
Total	47

Commute

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sum_left` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid`	—	`symm` `sum_right`
`sum_right` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid`	—	`multiset_sum_right` `Multiset.mem_map`

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dvd_sum` 📖	mathematical	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero`	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring`	—	`Multiset.dvd_sum` `Multiset.mem_map`
`mul_sum` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `sum` `NonUnitalNonAssocSemiring.toAddCommMonoid`	—	`map_sum` `AddMonoidHom.instAddMonoidHomClass`
`natCast_card_filter` 📖	mathematical	—	`AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `card` `filter` `sum` `AddCommMonoidWithOne.toAddCommMonoid` `AddMonoidWithOne.toOne` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid`	—	`sum_ite` `sum_const_zero` `add_zero` `sum_const` `nsmul_one`
`prod_add` 📖	mathematical	—	`prod` `CommSemiring.toCommMonoid` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `sum` `Finset` `NonUnitalNonAssocSemiring.toAddCommMonoid` `powerset` `Distrib.toMul` `instSDiff`	—	`prod_congr` `sum_insert` `sum_singleton` `prod_sum` `sum_bij'` `filter.congr_simp` `mem_filter` `prod_ite` `filter_subset` `Subtype.map_injective` `filter_attach'` `prod_map` `prod_attach` `ext`
`prod_add_one` 📖	mathematical	—	`prod` `CommSemiring.toCommMonoid` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `sum` `Finset` `NonUnitalNonAssocSemiring.toAddCommMonoid` `powerset`	—	`prod_add` `sum_congr` `prod_const_one` `mul_one`
`prod_add_ordered` 📖	mathematical	—	`prod` `CommSemiring.toCommMonoid` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Distrib.toMul` `filter` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrder.toDecidableLT`	—	`induction_on_max` `sum_congr` `prod_congr` `filter_empty` `mul_one` `add_zero` `lt_irrefl` `prod_insert` `sum_insert` `filter_insert` `filter_true_of_mem` `add_mul` `Distrib.rightDistribClass` `mul_add` `Distrib.leftDistribClass` `add_assoc` `add_comm` `filter_false_of_mem` `forall_mem_insert` `LT.lt.not_gt` `prod_empty` `mul_sum` `mem_filter` `mul_left_comm`
`prod_add_prod_eq` 📖	mathematical	`Finset` `SetLike.instMembership` `instSetLike` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `prod` `CommSemiring.toCommMonoid`	—	`prod_eq_mul_prod_diff_singleton_of_mem` `right_distrib` `Distrib.rightDistribClass` `prod_congr`
`prod_natCast` 📖	mathematical	—	`AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `prod` `Nat.instCommMonoid` `CommSemiring.toCommMonoid`	—	`map_prod` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`prod_neg` 📖	mathematical	—	`prod` `InvolutiveNeg.toNeg` `HasDistribNeg.toInvolutiveNeg` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `Monoid.toPow` `MulOne.toOne` `card`	—	`Multiset.map_map` `Multiset.map_congr` `Multiset.card_map` `Multiset.prod_map_neg`
`prod_one_add` 📖	mathematical	—	`prod` `CommSemiring.toCommMonoid` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `sum` `Finset` `NonUnitalNonAssocSemiring.toAddCommMonoid` `powerset`	—	`prod_congr` `add_comm` `prod_add` `sum_congr` `prod_const_one` `mul_one`
`prod_one_add_ordered` 📖	mathematical	—	`prod` `CommSemiring.toCommMonoid` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Distrib.toMul` `filter` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrder.toDecidableLT`	—	`prod_add_ordered` `prod_const_one` `sum_congr` `mul_one`
`prod_one_sub_ordered` 📖	mathematical	—	`prod` `CommRing.toCommMonoid` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `filter` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrder.toDecidableLT`	—	`prod_sub_ordered` `prod_const_one` `sum_congr` `mul_one`
`prod_range_natCast_sub` 📖	mathematical	—	`prod` `CommRing.toCommMonoid` `range` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Nat.instCommMonoid`	—	`prod_natCast` `le_or_gt` `prod_congr` `Nat.cast_sub` `LE.le.trans` `LT.lt.le` `mem_range` `prod_eq_zero` `sub_self` `Nat.cast_zero`
`prod_sub` 📖	mathematical	—	`prod` `CommRing.toCommMonoid` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `sum` `Finset` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `powerset` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `card` `instSDiff`	—	`prod_congr` `sub_eq_neg_add` `prod_add` `sum_congr` `prod_neg` `mul_right_comm`
`prod_sub_ordered` 📖	mathematical	—	`prod` `CommRing.toCommMonoid` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `filter` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrder.toDecidableLT`	—	`prod_congr` `sub_eq_add_neg` `sum_congr` `neg_mul` `sum_neg_distrib` `prod_add_ordered`
`prod_sum` 📖	mathematical	—	`prod` `CommSemiring.toCommMonoid` `sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `pi` `Finset` `SetLike.instMembership` `instSetLike` `attach`	—	`induction` `sum_congr` `sum_const` `card_singleton` `nsmul_eq_mul` `Nat.cast_one` `mul_one` `mem_insert_self` `Pi.cons_same` `prod_insert` `pi_insert` `sum_mul` `sum_biUnion` `Pi.cons_injective` `sum_image` `mul_sum` `mem_insert_of_mem` `attach_insert` `prod_image` `prod_congr` `mem_insert` `Pi.cons_ne`
`prod_univ_sum` 📖	mathematical	—	`prod` `CommSemiring.toCommMonoid` `univ` `sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Fintype.piFinset`	—	`prod_sum` `mem_univ` `sum_congr` `prod_attach_univ` `prod_congr` `sum_univ_pi`
`sum_boole` 📖	mathematical	—	`sum` `AddCommMonoidWithOne.toAddCommMonoid` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddMonoidWithOne.toNatCast` `card` `filter`	—	`natCast_card_filter`
`sum_boole_mul` 📖	mathematical	—	`sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `Finset` `SetLike.instMembership` `instSetLike` `decidableMem`	—	`sum_congr` `ite_mul` `one_mul` `MulZeroClass.zero_mul` `sum_ite_eq`
`sum_mul` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `sum` `NonUnitalNonAssocSemiring.toAddCommMonoid`	—	`map_sum` `AddMonoidHom.instAddMonoidHomClass`
`sum_mul_boole` 📖	mathematical	—	`sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `Finset` `SetLike.instMembership` `instSetLike` `decidableMem`	—	`sum_congr` `mul_ite` `mul_one` `MulZeroClass.mul_zero` `sum_ite_eq`
`sum_mul_sum` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `sum` `NonUnitalNonAssocSemiring.toAddCommMonoid`	—	`sum_mul` `sum_congr`
`sum_pow'` 📖	mathematical	—	`Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Fintype.piFinset` `Fin.fintype` `prod` `CommSemiring.toCommMonoid` `univ`	—	`prod_const` `Fintype.card_fin` `prod_univ_sum`
`sum_pow_mul_eq_add_pow` 📖	mathematical	—	`sum` `Finset` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `powerset` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `card` `Distrib.toAdd`	—	`prod_const` `prod_add` `sum_congr` `card_sdiff_of_subset` `mem_powerset`
`sum_prod_piFinset` 📖	mathematical	—	`sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Fintype.piFinset` `prod` `CommSemiring.toCommMonoid` `univ`	—	`prod_univ_sum`
`sum_range_succ_mul_sum_range_succ` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `range` `Distrib.toAdd`	—	`sum_range_succ` `mul_add` `Distrib.leftDistribClass` `add_mul` `Distrib.rightDistribClass` `add_assoc`

Fintype

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prod_add` 📖	mathematical	—	`Finset.prod` `CommSemiring.toCommMonoid` `Finset.univ` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Finset.sum` `Finset` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finset.fintype` `Distrib.toMul` `Compl.compl` `BooleanAlgebra.toCompl` `Finset.booleanAlgebra`	—	`Finset.sum_congr` `Finset.powerset_univ` `Finset.prod_add`
`prod_sum` 📖	mathematical	—	`Finset.prod` `CommSemiring.toCommMonoid` `Finset.univ` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Pi.instFintype`	—	`Finset.prod_univ_sum`
`sum_mul_sum` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finset.univ`	—	`Finset.sum_mul_sum`
`sum_pow` 📖	mathematical	—	`Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finset.univ` `Pi.instFintype` `Fin.fintype` `Finset.prod` `CommSemiring.toCommMonoid`	—	`Finset.sum_pow'`
`sum_pow_mul_eq_add_pow` 📖	mathematical	—	`Finset.sum` `Finset` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Finset.univ` `Finset.fintype` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Finset.card` `card` `Distrib.toAdd`	—	`Finset.sum_pow_mul_eq_add_pow`

Int

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cast_list_prod` 📖	mathematical	—	`AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `instRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`map_list_prod` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`cast_list_sum` 📖	mathematical	—	`AddGroupWithOne.toIntCast` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instCommRing` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddGroupWithOne.toAddGroup`	—	`map_list_sum` `AddMonoidHom.instAddMonoidHomClass`
`cast_multiset_prod` 📖	mathematical	—	`AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `CommRing.toRing` `Multiset.prod` `instCommMonoid` `CommRing.toCommMonoid` `Multiset.map`	—	`map_multiset_prod` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`cast_multiset_sum` 📖	mathematical	—	`AddGroupWithOne.toIntCast` `AddCommGroupWithOne.toAddGroupWithOne` `Multiset.sum` `instAddCommMonoid` `AddCommMonoidWithOne.toAddCommMonoid` `AddCommGroupWithOne.toAddCommMonoidWithOne` `Multiset.map`	—	`map_multiset_sum` `AddMonoidHom.instAddMonoidHomClass`
`cast_prod` 📖	mathematical	—	`AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `CommRing.toRing` `Finset.prod` `instCommMonoid` `CommRing.toCommMonoid`	—	`map_prod` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`cast_sum` 📖	mathematical	—	`AddGroupWithOne.toIntCast` `AddCommGroupWithOne.toAddGroupWithOne` `Finset.sum` `instAddCommMonoid` `AddCommMonoidWithOne.toAddCommMonoid` `AddCommGroupWithOne.toAddCommMonoidWithOne`	—	`map_sum` `AddMonoidHom.instAddMonoidHomClass`
`sum_div` 📖	mathematical	—	`Finset.sum` `instAddCommMonoid`	—	`eq_or_ne` `Finset.sum_congr` `Finset.sum_const_zero` `Finset.dvd_sum` `Finset.sum_mul`

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cast_list_prod` 📖	mathematical	—	`AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `instOne` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `AddMonoidWithOne.toOne`	—	`map_list_prod` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`cast_list_sum` 📖	mathematical	—	`AddMonoidWithOne.toNatCast` `MulZeroClass.toZero` `instMulZeroClass` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddMonoidWithOne.toAddMonoid` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`map_list_sum` `AddMonoidHom.instAddMonoidHomClass`
`cast_multiset_prod` 📖	mathematical	—	`AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Multiset.prod` `instCommMonoid` `CommSemiring.toCommMonoid` `Multiset.map`	—	`map_multiset_prod` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`cast_multiset_sum` 📖	mathematical	—	`AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `Multiset.sum` `instAddCommMonoid` `AddCommMonoidWithOne.toAddCommMonoid` `Multiset.map`	—	`map_multiset_sum` `AddMonoidHom.instAddMonoidHomClass`
`cast_prod` 📖	mathematical	—	`AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Finset.prod` `instCommMonoid` `CommSemiring.toCommMonoid`	—	`map_prod` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`cast_sum` 📖	mathematical	—	`AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `Finset.sum` `instAddCommMonoid` `AddCommMonoidWithOne.toAddCommMonoid`	—	`map_sum` `AddMonoidHom.instAddMonoidHomClass`
`sum_div` 📖	mathematical	—	`Finset.sum` `instAddCommMonoid`	—	`Finset.sum_congr` `Finset.sum_const_zero` `Finset.dvd_sum` `Finset.sum_mul`

---

← Back to Index