Basic

📁 Source: Mathlib/Algebra/BigOperators/Group/List/Basic.lean

Statistics

Metric	Count
Definitions	0
Theorems `list_sum_left`, `list_sum_right`, `map_list_sum`, `list_prod_left`, `list_prod_right`, `add_sum_eraseIdx`, `mul_prod_eraseIdx`, `prod_insertIdx`, `sum_insertIdx`, `prod_eq`, `sum_eq`, `add_sum_eraseIdx`, `alternatingProd_cons`, `alternatingProd_cons'`, `alternatingProd_cons_cons`, `alternatingProd_cons_cons'`, `alternatingProd_nil`, `alternatingProd_singleton`, `alternatingSum_cons`, `alternatingSum_cons'`, `alternatingSum_cons_cons`, `alternatingSum_cons_cons'`, `alternatingSum_nil`, `alternatingSum_singleton`, `drop_sum_flatten`, `eq_of_prod_take_eq`, `eq_of_sum_take_eq`, `exists_mem_ne_one_of_prod_ne_one`, `exists_mem_ne_zero_of_sum_ne_zero`, `getElem?_zero_add_tail_sum`, `getElem?_zero_mul_tail_prod`, `headI_add_tail_sum`, `headI_add_tail_sum_of_ne_nil`, `headI_le_sum`, `headI_mul_tail_prod_of_ne_nil`, `length_le_sum_of_one_le`, `length_pos_of_one_lt_prod`, `length_pos_of_prod_lt_one`, `length_pos_of_prod_ne_one`, `length_pos_of_sum_ne_zero`, `length_pos_of_sum_neg`, `length_pos_of_sum_pos`, `mul_prod_eraseIdx`, `prod_drop_succ`, `prod_eq_one`, `prod_eq_pow_single`, `prod_erase`, `prod_erase_of_comm`, `prod_hom`, `prod_hom_nonempty`, `prod_hom₂`, `prod_hom₂_nonempty`, `prod_insertIdx`, `prod_int_mod`, `prod_inv`, `prod_inv_reverse`, `prod_map_eq_pow_single`, `prod_map_erase`, `prod_map_filter_mul_prod_map_filter_not`, `prod_map_hom`, `prod_map_ite`, `prod_map_ite_eq`, `prod_map_mul`, `prod_mul_prod_eq_prod_zipWith_mul_prod_drop`, `prod_mul_prod_eq_prod_zipWith_of_length_eq`, `prod_nat_mod`, `prod_range_div`, `prod_range_div'`, `prod_range_succ`, `prod_range_succ'`, `prod_reverse`, `prod_reverse_noncomm`, `prod_set`, `prod_set'`, `prod_take_mul_prod_drop`, `prod_take_succ`, `prod_zpow`, `rel_prod`, `rel_sum`, `sum_add_sum_eq_sum_zipWith_add_sum_drop`, `sum_add_sum_eq_sum_zipWith_of_length_eq`, `sum_const_nat`, `sum_drop_succ`, `sum_eq_nsmul_single`, `sum_eq_zero`, `sum_erase`, `sum_erase_of_comm`, `sum_hom`, `sum_hom_nonempty`, `sum_hom₂`, `sum_hom₂_nonempty`, `sum_insertIdx`, `sum_int_mod`, `sum_map_add`, `sum_map_eq_nsmul_single`, `sum_map_erase`, `sum_map_filter_add_sum_map_filter_not`, `sum_map_hom`, `sum_map_ite`, `sum_map_ite_eq`, `sum_nat_mod`, `sum_neg`, `sum_neg_reverse`, `sum_range_sub`, `sum_range_sub'`, `sum_range_succ`, `sum_range_succ'`, `sum_reverse_noncomm`, `sum_set`, `sum_set'`, `sum_take_add_sum_drop`, `sum_take_succ`, `tail_sum`, `take_sum_flatten`, `map_list_prod`, `map_list_prod`, `map_list_sum`	117
Total	117

AddCommute

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`list_sum_left` 📖	mathematical	`AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddZero.toZero`	—	`symm` `list_sum_right`
`list_sum_right` 📖	mathematical	`AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddZero.toZero`	—	`zero_right` `add_right`

AddMonoidHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_list_sum` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instFunLike` `AddZero.toAdd` `AddZero.toZero`	—	`map_list_sum` `instAddMonoidHomClass`

Commute

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`list_prod_left` 📖	mathematical	`Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne`	—	`symm` `list_prod_right`
`list_prod_right` 📖	mathematical	`Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne`	—	`mul_right`

List

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_sum_eraseIdx` 📖	mathematical	`AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddZero.toZero`	—	`sum_insertIdx` `take_eraseIdx_eq_take_of_le` `insertIdx_eraseIdx_getElem`
`alternatingProd_cons` 📖	mathematical	—	`alternatingProd` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `InvOneClass.toInv` `DivInvMonoid.toDiv`	—	`div_eq_mul_inv` `alternatingProd_cons'`
`alternatingProd_cons'` 📖	mathematical	—	`alternatingProd` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `InvOneClass.toInv`	—	`alternatingProd_nil` `inv_one` `mul_one` `alternatingProd_singleton` `alternatingProd_cons_cons'` `mul_inv` `inv_inv` `mul_assoc`
`alternatingProd_cons_cons` 📖	mathematical	—	`alternatingProd` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `MulOne.toMul` `DivInvMonoid.toInv` `DivInvMonoid.toDiv`	—	`div_eq_mul_inv` `alternatingProd_cons_cons'`
`alternatingProd_cons_cons'` 📖	mathematical	—	`alternatingProd`	—	—
`alternatingProd_nil` 📖	mathematical	—	`alternatingProd`	—	—
`alternatingProd_singleton` 📖	mathematical	—	`alternatingProd`	—	—
`alternatingSum_cons` 📖	mathematical	—	`alternatingSum` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `NegZeroClass.toNeg` `SubNegMonoid.toSub`	—	`sub_eq_add_neg` `alternatingSum_cons'`
`alternatingSum_cons'` 📖	mathematical	—	`alternatingSum` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `NegZeroClass.toNeg`	—	`alternatingSum_nil` `neg_zero` `add_zero` `alternatingSum_singleton` `alternatingSum_cons_cons'` `neg_add` `neg_neg` `add_assoc`
`alternatingSum_cons_cons` 📖	mathematical	—	`alternatingSum` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddZero.toAdd` `SubNegMonoid.toNeg` `SubNegMonoid.toSub`	—	`sub_eq_add_neg` `alternatingSum_cons_cons'`
`alternatingSum_cons_cons'` 📖	mathematical	—	`alternatingSum`	—	—
`alternatingSum_nil` 📖	mathematical	—	`alternatingSum`	—	—
`alternatingSum_singleton` 📖	mathematical	—	`alternatingSum`	—	—
`drop_sum_flatten` 📖	mathematical	—	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid`	—	—
`eq_of_prod_take_eq` 📖	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `LeftCancelMonoid.toMonoid` `MulOne.toOne`	—	—	`mul_left_cancel` `LeftCancelSemigroup.toIsLeftCancelMul` `prod_take_succ`
`eq_of_sum_take_eq` 📖	—	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddLeftCancelMonoid.toAddMonoid` `AddZero.toZero`	—	—	`add_left_cancel` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `sum_take_succ`
`exists_mem_ne_one_of_prod_ne_one` 📖	—	—	—	—	`prod_eq_one`
`exists_mem_ne_zero_of_sum_ne_zero` 📖	—	—	—	—	`sum_eq_zero`
`getElem?_zero_add_tail_sum` 📖	mathematical	—	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddZero.toZero`	—	`add_zero`
`getElem?_zero_mul_tail_prod` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne`	—	`mul_one`
`headI_add_tail_sum` 📖	mathematical	—	`headI` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid`	—	`add_zero`
`headI_add_tail_sum_of_ne_nil` 📖	mathematical	—	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `headI` `AddZero.toZero`	—	—
`headI_le_sum` 📖	mathematical	—	`headI` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid`	—	`headI_add_tail_sum`
`headI_mul_tail_prod_of_ne_nil` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `headI` `MulOne.toOne`	—	—
`length_le_sum_of_one_le` 📖	mathematical	—	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid`	—	`add_comm`
`length_pos_of_one_lt_prod` 📖	—	`Preorder.toLT` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toMul`	—	—	`length_pos_of_prod_ne_one` `LT.lt.ne'`
`length_pos_of_prod_lt_one` 📖	—	`Preorder.toLT` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne`	—	—	`length_pos_of_prod_ne_one` `LT.lt.ne`
`length_pos_of_prod_ne_one` 📖	—	—	—	—	—
`length_pos_of_sum_ne_zero` 📖	—	—	—	—	—
`length_pos_of_sum_neg` 📖	—	`Preorder.toLT` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddZero.toZero`	—	—	`length_pos_of_sum_ne_zero` `LT.lt.ne`
`length_pos_of_sum_pos` 📖	—	`Preorder.toLT` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddZero.toAdd`	—	—	`length_pos_of_sum_ne_zero` `LT.lt.ne'`
`mul_prod_eraseIdx` 📖	mathematical	`Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne`	—	`prod_insertIdx` `take_eraseIdx_eq_take_of_le` `insertIdx_eraseIdx_getElem`
`prod_drop_succ` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `InvOneClass.toInv`	—	`zero_add` `inv_mul_cancel_left`
`prod_eq_one` 📖	mathematical	`MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne`	—	`one_mul`
`prod_eq_pow_single` 📖	mathematical	`MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne` `Monoid.toPow`	—	`trans` `IsPreorder.toIsTrans` `IsEquiv.toIsPreorder` `eq_isEquiv` `prod_map_eq_pow_single`
`prod_erase` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `MulOne.toOne`	—	`prod_erase_of_comm` `mul_comm`
`prod_erase_of_comm` 📖	mathematical	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne`	—	`mul_assoc`
`prod_hom` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne` `DFunLike.coe`	—	`map_one` `MonoidHomClass.toOneHomClass` `map_mul` `MonoidHomClass.toMulHomClass`
`prod_hom_nonempty` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne` `DFunLike.coe`	—	`mul_one` `map_mul`
`prod_hom₂` 📖	mathematical	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne`	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne`	—	`foldr_hom₂`
`prod_hom₂_nonempty` 📖	mathematical	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne`	—	`mul_one`
`prod_insertIdx` 📖	mathematical	`Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne`	—	`Commute.left_comm` `Commute.symm`
`prod_int_mod` 📖	mathematical	—	`MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Int.instMonoid`	—	—
`prod_inv` 📖	mathematical	—	`InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `DivisionMonoid.toDivInvMonoid` `InvOneClass.toOne`	—	`inv_one` `mul_inv_rev` `mul_comm`
`prod_inv_reverse` 📖	mathematical	—	`InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `InvOneClass.toOne`	—	`inv_one` `mul_inv_rev` `Semigroup.to_isLawfulIdentity` `Semigroup.to_isAssociative` `mul_one`
`prod_map_eq_pow_single` 📖	mathematical	`MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne` `Monoid.toPow`	—	`pow_zero` `pow_succ'` `one_mul` `add_zero`
`prod_map_erase` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `MulOne.toOne`	—	`not_beq_of_ne` `mul_left_comm`
`prod_map_filter_mul_prod_map_filter_not` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `MulOne.toOne`	—	`prod_map_ite`
`prod_map_hom` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne` `DFunLike.coe`	—	`prod_hom`
`prod_map_ite` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `MulOne.toOne`	—	`mul_one` `mul_assoc` `mul_left_comm`
`prod_map_ite_eq` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `Monoid.toPow` `DivInvMonoid.toDiv`	—	`pow_zero` `mul_one` `div_eq_mul_inv` `pow_add` `pow_one` `mul_comm` `mul_assoc` `mul_left_comm` `mul_inv_cancel_left` `add_zero`
`prod_map_mul` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `MulOne.toOne`	—	`prod_hom₂` `mul_mul_mul_comm` `mul_one`
`prod_mul_prod_eq_prod_zipWith_mul_prod_drop` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `MulOne.toOne`	—	`one_mul` `mul_one` `mul_assoc` `mul_comm`
`prod_mul_prod_eq_prod_zipWith_of_length_eq` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `MulOne.toOne`	—	`prod_mul_prod_eq_prod_zipWith_mul_prod_drop` `mul_one`
`prod_nat_mod` 📖	mathematical	—	`Nat.instOne`	—	—
`prod_range_div` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `DivInvMonoid.toDiv`	—	`inv_div` `prod_inv` `prod_range_div'`
`prod_range_div'` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `DivInvMonoid.toDiv`	—	`div_self'` `Semigroup.to_isLawfulIdentity` `Semigroup.to_isAssociative` `mul_one` `div_mul_div_cancel`
`prod_range_succ` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne`	—	`Semigroup.to_isLawfulIdentity` `Semigroup.to_isAssociative` `mul_one`
`prod_range_succ'` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne`	—	—
`prod_reverse` 📖	—	—	—	—	—
`prod_reverse_noncomm` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `InvOneClass.toInv`	—	`prod_inv_reverse` `Function.Involutive.comp_self`
`prod_set` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne`	—	`one_mul` `zero_add` `mul_ite` `mul_one` `ite_mul` `mul_assoc`
`prod_set'` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `InvOneClass.toInv`	—	`prod_set` `mul_comm` `mul_assoc` `prod_drop_succ` `prod_take_mul_prod_drop` `mul_one`
`prod_take_mul_prod_drop` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne`	—	`Semigroup.to_isLawfulIdentity` `Semigroup.to_isAssociative`
`prod_take_succ` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne`	—	`take_concat_get'` `Semigroup.to_isLawfulIdentity` `Semigroup.to_isAssociative` `mul_one`
`prod_zpow` 📖	mathematical	—	`DivInvMonoid.toZPow` `DivisionMonoid.toDivInvMonoid` `DivisionCommMonoid.toDivisionMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid`	—	`one_zpow` `mul_zpow` `map_list_prod` `MonoidHom.instMonoidHomClass`
`rel_prod` 📖	mathematical	`MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Relator.LiftFun` `MulOne.toMul`	`Relator.LiftFun` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne`	—	`rel_foldr`
`rel_sum` 📖	mathematical	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Relator.LiftFun` `AddZero.toAdd`	`Relator.LiftFun` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddZero.toZero`	—	`rel_foldr`
`sum_add_sum_eq_sum_zipWith_add_sum_drop` 📖	mathematical	—	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddZero.toZero`	—	`zero_add` `add_zero` `add_assoc` `add_comm`
`sum_add_sum_eq_sum_zipWith_of_length_eq` 📖	mathematical	—	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddZero.toZero`	—	`sum_add_sum_eq_sum_zipWith_add_sum_drop` `add_zero`
`sum_const_nat` 📖	mathematical	—	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid`	—	`sum_replicate`
`sum_drop_succ` 📖	mathematical	—	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `NegZeroClass.toNeg`	—	`zero_add` `neg_add_cancel_left`
`sum_eq_nsmul_single` 📖	mathematical	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddZero.toZero` `AddMonoid.toNSMul`	—	`trans` `IsPreorder.toIsTrans` `IsEquiv.toIsPreorder` `eq_isEquiv` `sum_map_eq_nsmul_single`
`sum_eq_zero` 📖	mathematical	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddZero.toZero`	—	`zero_add`
`sum_erase` 📖	mathematical	—	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddZero.toZero`	—	`sum_erase_of_comm` `add_comm`
`sum_erase_of_comm` 📖	mathematical	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddZero.toZero`	—	`add_assoc`
`sum_hom` 📖	mathematical	—	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddZero.toZero` `DFunLike.coe`	—	`map_zero` `AddMonoidHomClass.toZeroHomClass` `map_add` `AddMonoidHomClass.toAddHomClass`
`sum_hom_nonempty` 📖	mathematical	—	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddZero.toZero` `DFunLike.coe`	—	`add_zero` `map_add`
`sum_hom₂` 📖	mathematical	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddZero.toZero`	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddZero.toZero`	—	`foldr_hom₂`
`sum_hom₂_nonempty` 📖	mathematical	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddZero.toZero`	—	`add_zero`
`sum_insertIdx` 📖	mathematical	`AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddZero.toZero`	—	`AddCommute.left_comm` `AddCommute.symm`
`sum_int_mod` 📖	mathematical	—	`NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Int.instAddCommGroup`	—	—
`sum_map_add` 📖	mathematical	—	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddZero.toZero`	—	`sum_hom₂` `add_add_add_comm` `add_zero`
`sum_map_eq_nsmul_single` 📖	mathematical	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddZero.toZero` `AddMonoid.toNSMul`	—	`zero_nsmul` `succ_nsmul'` `zero_add` `add_zero`
`sum_map_erase` 📖	mathematical	—	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddZero.toZero`	—	`not_beq_of_ne` `add_left_comm`
`sum_map_filter_add_sum_map_filter_not` 📖	mathematical	—	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddZero.toZero`	—	`sum_map_ite`
`sum_map_hom` 📖	mathematical	—	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddZero.toZero` `DFunLike.coe`	—	`sum_hom`
`sum_map_ite` 📖	mathematical	—	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddZero.toZero`	—	`add_zero` `add_assoc` `add_left_comm`
`sum_map_ite_eq` 📖	mathematical	—	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `AddMonoid.toNSMul` `SubNegMonoid.toSub`	—	`zero_nsmul` `add_zero` `sub_eq_add_neg` `add_nsmul` `one_nsmul` `add_comm` `add_assoc` `add_left_comm` `add_neg_cancel_left`
`sum_nat_mod` 📖	mathematical	—	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid`	—	—
`sum_neg` 📖	mathematical	—	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `SubtractionMonoid.toSubNegMonoid` `NegZeroClass.toZero`	—	`neg_zero` `neg_add_rev` `add_comm`
`sum_neg_reverse` 📖	mathematical	—	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `NegZeroClass.toZero`	—	`neg_zero` `neg_add_rev` `AddSemigroup.to_isLawfulIdentity` `AddSemigroup.to_isAssociative` `add_zero`
`sum_range_sub` 📖	mathematical	—	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SubNegMonoid.toSub`	—	`neg_sub` `sum_neg` `sum_range_sub'`
`sum_range_sub'` 📖	mathematical	—	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `SubNegMonoid.toSub`	—	`sub_self` `AddSemigroup.to_isLawfulIdentity` `AddSemigroup.to_isAssociative` `add_zero` `sub_add_sub_cancel`
`sum_range_succ` 📖	mathematical	—	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddZero.toZero`	—	`AddSemigroup.to_isLawfulIdentity` `AddSemigroup.to_isAssociative` `add_zero`
`sum_range_succ'` 📖	mathematical	—	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddZero.toZero`	—	—
`sum_reverse_noncomm` 📖	mathematical	—	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `NegZeroClass.toNeg`	—	`sum_neg_reverse` `Function.Involutive.comp_self` `neg_involutive`
`sum_set` 📖	mathematical	—	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddZero.toZero`	—	`zero_add` `add_ite` `add_zero` `ite_add` `add_assoc`
`sum_set'` 📖	mathematical	—	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NegZeroClass.toNeg`	—	`sum_set` `add_comm` `add_assoc` `sum_drop_succ` `sum_take_add_sum_drop` `add_zero`
`sum_take_add_sum_drop` 📖	mathematical	—	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddZero.toZero`	—	`AddSemigroup.to_isLawfulIdentity` `AddSemigroup.to_isAssociative`
`sum_take_succ` 📖	mathematical	—	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddZero.toZero`	—	`take_concat_get'` `AddSemigroup.to_isLawfulIdentity` `AddSemigroup.to_isAssociative` `add_zero`
`tail_sum` 📖	mathematical	—	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `headI`	—	`headI_add_tail_sum` `add_comm`
`take_sum_flatten` 📖	mathematical	—	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid`	—	—

List.CommMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_sum_eraseIdx` 📖	mathematical	—	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddZero.toZero`	—	`List.add_sum_eraseIdx` `AddCommute.all`
`mul_prod_eraseIdx` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `MulOne.toOne`	—	`List.mul_prod_eraseIdx` `Commute.all`
`prod_insertIdx` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `MulOne.toOne`	—	`List.prod_insertIdx` `Commute.all`
`sum_insertIdx` 📖	mathematical	—	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddZero.toZero`	—	`List.sum_insertIdx` `AddCommute.all`

List.Perm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prod_eq` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `MulOne.toOne`	—	`foldr_op_eq` `Semigroup.to_isAssociative` `CommMagma.to_isCommutative`
`sum_eq` 📖	mathematical	—	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddZero.toZero`	—	`foldr_op_eq` `AddSemigroup.to_isAssociative` `AddCommMagma.to_isCommutative`

MonoidHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_list_prod` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instFunLike` `MulOne.toMul` `MulOne.toOne`	—	`map_list_prod` `instMonoidHomClass`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_list_prod` 📖	mathematical	—	`DFunLike.coe` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne`	—	`List.prod_hom`
`map_list_sum` 📖	mathematical	—	`DFunLike.coe` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddZero.toZero`	—	`List.sum_hom`

---

← Back to Index