Documentation Verification Report

Pi

📁 Source: Mathlib/Algebra/BigOperators/Pi.lean

Statistics

Metric	Count
Definitions `addMonoidHomAddEquiv`, `monoidHomMulEquiv`	2
Theorems `functions_ext`, `functions_ext'`, `functions_ext'_iff`, `prod_apply`, `prod_fn`, `sum_apply`, `sum_fn`, `univ_prod_mulSingle`, `univ_sum_single`, `prod_apply`, `sum_apply`, `functions_ext`, `functions_ext'`, `functions_ext'_iff`, `list_prod_apply`, `list_sum_apply`, `mulSingle_induction`, `multiset_prod_apply`, `multiset_sum_apply`, `single_induction`, `fst_prod`, `fst_sum`, `snd_prod`, `snd_sum`, `functions_ext`, `functions_ext_iff`, `eqOn_finsetProd`, `eqOn_finsetSum`, `eqOn_fun_finsetProd`, `eqOn_fun_finsetSum`, `pi_eq_sum_univ`, `pi_eq_sum_univ'`, `prod_indicator`, `prod_indicator_apply`, `prod_indicator_const`, `prod_indicator_const_apply`, `prod_mk_prod`, `prod_mk_sum`	38
Total	40

AddMonoidHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`functions_ext` 📖	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `Pi.addZeroClass` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instFunLike` `Pi.single` `AddZero.toZero`	—	—	`nonempty_fintype` `ext` `Finset.univ_sum_single` `map_sum` `instAddMonoidHomClass` `Finset.sum_congr`
`functions_ext'` 📖	—	`comp` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Pi.addZeroClass` `single`	—	—	`functions_ext` `DFunLike.congr_fun`
`functions_ext'_iff` 📖	mathematical	—	`comp` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Pi.addZeroClass` `single`	—	`functions_ext'`

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prod_apply` 📖	mathematical	—	`prod` `Pi.commMonoid`	—	`map_prod` `MonoidHom.instMonoidHomClass`
`prod_fn` 📖	mathematical	—	`prod` `Pi.commMonoid`	—	`prod_apply`
`sum_apply` 📖	mathematical	—	`sum` `Pi.addCommMonoid`	—	`map_sum` `AddMonoidHom.instAddMonoidHomClass`
`sum_fn` 📖	mathematical	—	`sum` `Pi.addCommMonoid`	—	`sum_apply`
`univ_prod_mulSingle` 📖	mathematical	—	`prod` `Pi.commMonoid` `univ` `Pi.mulSingle` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid`	—	`prod_apply` `prod_pi_mulSingle`
`univ_sum_single` 📖	mathematical	—	`sum` `Pi.addCommMonoid` `univ` `Pi.single` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`sum_apply` `sum_pi_single` `mem_univ`

Fintype

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prod_apply` 📖	mathematical	—	`Finset.prod` `Pi.commMonoid` `Finset.univ`	—	`Finset.prod_apply`
`sum_apply` 📖	mathematical	—	`Finset.sum` `Pi.addCommMonoid` `Finset.univ`	—	`Finset.sum_apply`

MonoidHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`functions_ext` 📖	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Pi.mulOneClass` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `instFunLike` `Pi.mulSingle` `MulOne.toOne`	—	—	`nonempty_fintype` `ext` `Finset.univ_prod_mulSingle` `map_prod` `instMonoidHomClass` `Finset.prod_congr`
`functions_ext'` 📖	—	`comp` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `Pi.mulOneClass` `mulSingle`	—	—	`functions_ext` `DFunLike.congr_fun`
`functions_ext'_iff` 📖	mathematical	—	`comp` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `Pi.mulOneClass` `mulSingle`	—	`functions_ext'`

Pi

Definitions

Name	Category	Theorems
`addMonoidHomAddEquiv` 📖	CompOp	—
`monoidHomMulEquiv` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`list_prod_apply` 📖	mathematical	—	`instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instOne` `MulOne.toOne`	—	`map_list_prod` `MonoidHom.instMonoidHomClass`
`list_sum_apply` 📖	mathematical	—	`instAdd` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instZero` `AddZero.toZero`	—	`map_list_sum` `AddMonoidHom.instAddMonoidHomClass`
`mulSingle_induction` 📖	—	`instOne` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `instMul` `MulOne.toMul` `mulSingle`	—	—	`nonempty_fintype` `Finset.univ_prod_mulSingle` `Finset.prod_induction`
`multiset_prod_apply` 📖	mathematical	—	`Multiset.prod` `commMonoid` `Multiset.map`	—	`MonoidHom.map_multiset_prod`
`multiset_sum_apply` 📖	mathematical	—	`Multiset.sum` `addCommMonoid` `Multiset.map`	—	`AddMonoidHom.map_multiset_sum`
`single_induction` 📖	—	`instZero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `single`	—	—	`nonempty_fintype` `Finset.univ_sum_single` `Finset.sum_induction`

Prod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fst_prod` 📖	mathematical	—	`Finset.prod` `instCommMonoid`	—	`map_prod` `MonoidHom.instMonoidHomClass`
`fst_sum` 📖	mathematical	—	`Finset.sum` `instAddCommMonoid`	—	`map_sum` `AddMonoidHom.instAddMonoidHomClass`
`snd_prod` 📖	mathematical	—	`Finset.prod` `instCommMonoid`	—	`map_prod` `MonoidHom.instMonoidHomClass`
`snd_sum` 📖	mathematical	—	`Finset.sum` `instAddCommMonoid`	—	`map_sum` `AddMonoidHom.instAddMonoidHomClass`

RingHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`functions_ext` 📖	—	`DFunLike.coe` `RingHom` `Pi.nonAssocSemiring` `instFunLike` `Pi.single` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	—	`coe_addMonoidHom_injective` `AddMonoidHom.functions_ext` `RingHomClass.toAddMonoidHomClass` `instRingHomClass`
`functions_ext_iff` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Pi.nonAssocSemiring` `instFunLike` `Pi.single` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`functions_ext`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eqOn_finsetProd` 📖	mathematical	`Set.EqOn`	`Finset.prod` `Pi.commMonoid`	—	`Finset.prod_apply`
`eqOn_finsetSum` 📖	mathematical	`Set.EqOn`	`Finset.sum` `Pi.addCommMonoid`	—	`Finset.sum_apply`
`eqOn_fun_finsetProd` 📖	mathematical	`Set.EqOn`	`Finset.prod`	—	`Finset.prod_apply` `eqOn_finsetProd`
`eqOn_fun_finsetSum` 📖	mathematical	`Set.EqOn`	`Finset.sum`	—	`Finset.sum_apply` `eqOn_finsetSum`
`pi_eq_sum_univ` 📖	mathematical	—	`Finset.sum` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Finset.univ` `Function.hasSMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`Finset.sum_apply` `Finset.sum_congr` `mul_ite` `mul_one` `MulZeroClass.mul_zero` `Finset.sum_ite_eq'`
`pi_eq_sum_univ'` 📖	mathematical	—	`Finset.sum` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Finset.univ` `Function.hasSMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Pi.single` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`Finset.sum_congr` `Pi.single_eq_of_ne'` `Pi.single_eq_same` `pi_eq_sum_univ`
`prod_indicator` 📖	mathematical	—	`Finset.prod` `Pi.commMonoid` `CommSemiring.toCommMonoid` `Set.indicator` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Set.iInter` `Finset` `Finset.instMembership`	—	`Finset.prod_apply` `prod_indicator_apply`
`prod_indicator_apply` 📖	mathematical	—	`Finset.prod` `CommSemiring.toCommMonoid` `Set.indicator` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Set.iInter` `Finset` `Finset.instMembership` `Pi.commMonoid`	—	`Set.indicator.eq_1` `Finset.prod_apply` `Finset.prod_congr` `Set.indicator_of_mem` `Finset.prod_eq_zero` `Set.indicator_of_notMem`
`prod_indicator_const` 📖	mathematical	—	`Finset.prod` `Pi.commMonoid` `CommSemiring.toCommMonoid` `Set.indicator` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Set.iInter` `Finset` `Finset.instMembership` `Pi.instPow` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Finset.card`	—	`prod_indicator` `Finset.prod_const`
`prod_indicator_const_apply` 📖	mathematical	—	`Finset.prod` `CommSemiring.toCommMonoid` `Set.indicator` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Set.iInter` `Finset` `Finset.instMembership` `Pi.instPow` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Finset.card`	—	`prod_indicator_apply` `Finset.prod_const`
`prod_mk_prod` 📖	mathematical	—	`Finset.prod` `Prod.instCommMonoid`	—	`Finset.induction_on` `Finset.prod_insert`
`prod_mk_sum` 📖	mathematical	—	`Finset.sum` `Prod.instAddCommMonoid`	—	`Finset.induction_on` `Finset.sum_insert`

---

← Back to Index