Documentation Verification Report

Lemmas

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

Statistics

Metric	Count
Definitions	0
Theorems `prod_eq'`, `sum_eq'`, `prod_dvd_prod`, `alternatingProd_append`, `alternatingProd_reverse`, `alternatingSum_append`, `alternatingSum_reverse`, `drop_take_succ_flatten_eq_getElem`, `dvd_prod`, `length_sigma`, `mem_mem_ranges_iff_lt_sum`, `neg_one_mem_of_prod_eq_neg_one`, `prod_isUnit`, `prod_isUnit_iff`, `prod_rotate_eq_one_of_prod_eq_one`, `ranges_flatten`, `ranges_nodup`, `sum_isAddUnit`, `sum_isAddUnit_iff`, `sum_map_count_dedup_eq_length`, `sum_map_count_dedup_filter_eq_countP`, `op_list_prod`, `unop_list_prod`, `unop_map_list_prod`	24
Total	24

List

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`alternatingProd_append` 📖	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.toZPow` `Monoid.toNatPow` `Int.instMonoid`	—	`pow_zero` `zpow_one` `one_mul` `alternatingProd_cons` `pow_succ'` `zpow_neg` `div_div`
`alternatingProd_reverse` 📖	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.toZPow` `Monoid.toNatPow` `Int.instMonoid`	—	`one_zpow` `alternatingProd_append` `alternatingProd_cons` `pow_succ'` `one_mul` `zpow_neg` `inv_inv` `mul_comm` `div_eq_mul_inv` `div_zpow`
`alternatingSum_append` 📖	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.toZSMul` `Monoid.toNatPow` `Int.instMonoid`	—	`pow_zero` `one_zsmul` `zero_add` `alternatingSum_cons` `pow_succ'` `one_mul` `neg_zsmul` `sub_eq_add_neg` `sub_sub`
`alternatingSum_reverse` 📖	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.toZSMul` `Monoid.toNatPow` `Int.instMonoid`	—	`zsmul_zero` `alternatingSum_append` `alternatingSum_cons` `pow_succ'` `one_mul` `neg_zsmul` `neg_neg` `add_comm` `sub_eq_add_neg` `zsmul_sub`
`drop_take_succ_flatten_eq_getElem` 📖	mathematical	—	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid`	—	`take_sum_flatten` `drop_sum_flatten` `drop_take_succ_eq_cons_getElem`
`dvd_prod` 📖	mathematical	—	`semigroupDvd` `Monoid.toSemigroup` `CommMonoid.toMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne`	—	`Semigroup.to_isLawfulIdentity` `Semigroup.to_isAssociative` `mul_left_comm` `dvd_mul_right`
`length_sigma` 📖	mathematical	—	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid`	—	—
`mem_mem_ranges_iff_lt_sum` 📖	mathematical	—	`ranges` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid`	—	`ranges_flatten`
`neg_one_mem_of_prod_eq_neg_one` 📖	—	`MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Int.instMonoid`	—	—	`exists_mem_ne_one_of_prod_ne_one` `ne_of_eq_of_ne` `Int.isUnit_iff` `prod_isUnit_iff`
`prod_isUnit` 📖	mathematical	`IsUnit`	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne`	—	`IsUnit.mul`
`prod_isUnit_iff` 📖	mathematical	—	`IsUnit` `CommMonoid.toMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne`	—	`IsUnit.mul_iff` `instIsDedekindFiniteMonoid` `prod_isUnit`
`prod_rotate_eq_one_of_prod_eq_one` 📖	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	—	`rotate_nil` `le_of_lt` `rotate_mod` `rotate_eq_drop_append_take` `Semigroup.to_isLawfulIdentity` `Semigroup.to_isAssociative` `mul_eq_one_iff_inv_eq` `one_mul` `mul_assoc` `mul_inv_cancel` `mul_one`
`ranges_flatten` 📖	mathematical	—	`ranges` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid`	—	—
`ranges_nodup` 📖	—	`ranges`	—	—	`ranges_flatten`
`sum_isAddUnit` 📖	mathematical	`IsAddUnit`	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddZero.toZero`	—	`isAddUnit_zero` `IsAddUnit.add`
`sum_isAddUnit_iff` 📖	mathematical	—	`IsAddUnit` `AddCommMonoid.toAddMonoid` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddZero.toZero`	—	`IsAddUnit.add_iff` `instIsDedekindFiniteAddMonoid` `sum_isAddUnit`
`sum_map_count_dedup_eq_length` 📖	mathematical	—	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `dedup`	—	`filter_true` `sum_map_count_dedup_filter_eq_countP`
`sum_map_count_dedup_filter_eq_countP` 📖	mathematical	—	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `dedup`	—	`sum_map_add` `trans` `IsPreorder.toIsTrans` `IsEquiv.toIsPreorder` `eq_isEquiv` `dedup_cons_of_mem` `dedup_cons_of_notMem` `zero_add` `sum_map_eq_nsmul_single` `count_dedup` `mul_one` `sum_eq_zero`

List.Perm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prod_eq'` 📖	mathematical	`Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`MulOne.toOne`	—	`List.Pairwise.forall_of_forall` `mul_assoc`
`sum_eq'` 📖	mathematical	`AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`AddZero.toZero`	—	`List.Pairwise.forall_of_forall` `add_assoc`

List.Sublist

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prod_dvd_prod` 📖	mathematical	—	`semigroupDvd` `Monoid.toSemigroup` `CommMonoid.toMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne`	—	`List.Perm.prod_eq` `Semigroup.to_isLawfulIdentity` `Semigroup.to_isAssociative` `dvd_mul_right`

MulOpposite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`op_list_prod` 📖	mathematical	—	`op` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne` `MulOpposite` `instMul` `instOne`	—	`List.reverse_cons'` `Semigroup.to_isLawfulIdentity` `Semigroup.to_isAssociative` `op_mul`
`unop_list_prod` 📖	mathematical	—	`unop` `MulOpposite` `instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instOne` `MulOne.toOne`	—	`op_unop` `op_list_prod` `op_comp_unop`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`unop_map_list_prod` 📖	mathematical	—	`MulOpposite.unop` `DFunLike.coe` `MulOpposite` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne`	—	`map_list_prod` `MulOpposite.unop_list_prod`

---

← Back to Index