Documentation Verification Report

Defs

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

Statistics

Metric	Count
Definitions `alternatingProd`, `alternatingSum`	2
Theorems `prod_eq_pow_card`, `prod_hom_rel`, `prod_induction`, `prod_induction_nonempty`, `prod_map_one`, `prod_replicate`, `sum_eq_card_nsmul`, `sum_hom_rel`, `sum_induction`, `sum_induction_nonempty`, `sum_map_zero`, `sum_replicate`	12
Total	14

List

Definitions

Name	Category	Theorems
`alternatingProd` 📖	CompOp	9 math math: `alternatingProd_eq_finset_prod`, `alternatingProd_cons_cons`, `alternatingProd_nil`, `alternatingProd_append`, `alternatingProd_cons_cons'`, `alternatingProd_cons'`, `alternatingProd_cons`, `alternatingProd_reverse`, `alternatingProd_singleton`
`alternatingSum` 📖	CompOp	12 math math: `alternatingSum_append`, `alternatingSum_cons_cons`, `alternatingSum_cons_cons'`, `alternatingSum_singleton`, `alternatingSum_nil`, `alternatingSum_reverse`, `alternatingSum_cons`, `Nat.modEq_eleven_digits_sum`, `Nat.ofDigits_neg_one`, `alternatingSum_cons'`, `alternatingSum_eq_finset_sum`, `Nat.eleven_dvd_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prod_eq_pow_card` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne` `Monoid.toNatPow`	—	`prod_replicate`
`prod_hom_rel` 📖	—	`MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toMul`	—	—	—
`prod_induction` 📖	—	—	—	—	—
`prod_induction_nonempty` 📖	mathematical	`MulOne.toMul` `MulOneClass.toMulOne`	`MulOne.toOne`	—	`mul_one`
`prod_map_one` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `MulOne.toOne`	—	`mul_one`
`prod_replicate` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne` `Monoid.toNatPow`	—	`pow_zero` `pow_succ'`
`sum_eq_card_nsmul` 📖	mathematical	—	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddZero.toZero` `AddMonoid.toNatSMul`	—	`sum_replicate`
`sum_hom_rel` 📖	—	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddZero.toAdd`	—	—	—
`sum_induction` 📖	—	—	—	—	—
`sum_induction_nonempty` 📖	mathematical	`AddZero.toAdd` `AddZeroClass.toAddZero`	`AddZero.toZero`	—	`add_zero`
`sum_map_zero` 📖	mathematical	—	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddZero.toZero`	—	`add_zero`
`sum_replicate` 📖	mathematical	—	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddZero.toZero` `AddMonoid.toNatSMul`	—	`zero_nsmul` `succ_nsmul'`

---

← Back to Index