Finset

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

Statistics

Metric	Count
Definitions	0
Theorems prod_boole, prod_eq_zero, prod_eq_zero_iff, prod_ite_zero, prod_ne_zero_iff, support_prod, support_prod_subset, prod_boole, prod_ite_zero, indicator_pi_one_apply, mk0_prod	11
Total	11

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
prod_boole 📖	mathematical	—	prod CommMonoidWithZero.toCommMonoid MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero MulZeroClass.toZero MulZeroOneClass.toMulZeroClass decidableDforallFinset	—	prod_ite_zero prod_const_one
prod_eq_zero 📖	mathematical	Finset instMembership MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero	prod CommMonoidWithZero.toCommMonoid	—	prod_erase_mul MulZeroClass.mul_zero
prod_eq_zero_iff 📖	mathematical	—	prod CommMonoidWithZero.toCommMonoid MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero Finset instMembership	—	induction_on one_ne_zero NeZero.one prod_insert mul_eq_zero exists_mem_insert
prod_ite_zero 📖	mathematical	—	prod CommMonoidWithZero.toCommMonoid MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero decidableDforallFinset	—	prod_congr Mathlib.Tactic.Push.not_forall_eq prod_eq_zero
prod_ne_zero_iff 📖	—	—	—	—	prod_eq_zero_iff Mathlib.Tactic.Push.not_and_eq
support_prod 📖	mathematical	—	Function.support MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero prod CommMonoidWithZero.toCommMonoid Set.iInter Finset instMembership	—	Set.ext Set.iInter_congr_Prop
support_prod_subset 📖	mathematical	—	Set Set.instHasSubset Function.support MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero prod CommMonoidWithZero.toCommMonoid Set.iInter Finset instMembership	—	Set.mem_iInter₂ prod_eq_zero

Fintype

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
prod_boole 📖	mathematical	—	Finset.prod CommMonoidWithZero.toCommMonoid Finset.univ MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero MulZeroClass.toZero MulZeroOneClass.toMulZeroClass decidableForallFintype	—	Finset.prod_boole
prod_ite_zero 📖	mathematical	—	Finset.prod CommMonoidWithZero.toCommMonoid Finset.univ MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero decidableForallFintype	—	Finset.prod_ite_zero

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
indicator_pi_one_apply 📖	mathematical	—	indicator MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero pi SetLike.coe Finset Finset.instSetLike Pi.instOne MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass Finset.prod CommMonoidWithZero.toCommMonoid	—	Finset.prod_congr Finset.prod_boole

Units

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mk0_prod 📖	mathematical	—	CommGroupWithZero.toGroupWithZero Finset.prod CommMonoidWithZero.toCommMonoid CommGroupWithZero.toCommMonoidWithZero Finset Finset.instMembership Units MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero CommGroup.toCommMonoid instCommGroupUnits Finset.attach Finset.prod_eq_zero	—	Finset.cons_induction_on Finset.prod_eq_zero mul_ne_zero_iff GroupWithZero.noZeroDivisors Finset.prod_cons Finset.mem_cons_self Finset.mem_cons_of_mem Finset.prod_congr Finset.attach_cons Finset.prod_map

---

← Back to Index