Documentation Verification Report

Finset

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

Statistics

Metric	Count
Definitions	0
Theorems `le_prod_max_one`, `one_le_prod`, `prod_anti_set_of_le_one`, `prod_le_one`, `prod_le_prod`, `prod_le_prod_of_subset_of_le_one`, `prod_le_prod_of_subset_of_one_le`, `prod_lt_prod`, `prod_lt_prod_of_nonempty`, `prod_mono_set_of_one_le`, `prod_nonneg`, `prod_pos`	12
Total	12

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`le_prod_max_one` 📖	mathematical	`Finset` `SetLike.instMembership` `instSetLike`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `prod` `CommMonoidWithZero.toCommMonoid` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero`	—	`lt_or_ge` `LT.lt.le` `LT.lt.trans_le` `prod_nonneg` `le_sup_of_le_right` `zero_le_one` `prod_eq_single_of_mem` `prod_le_prod`
`one_le_prod` 📖	mathematical	`Preorder.toLE` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero`	`Preorder.toLE` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `prod` `CommMonoidWithZero.toCommMonoid`	—	`prod_const_one` `prod_le_prod`
`prod_anti_set_of_le_one` 📖	mathematical	`Preorder.toLE` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass`	`Antitone` `Finset` `PartialOrder.toPreorder` `partialOrder` `prod` `CommMonoidWithZero.toCommMonoid`	—	`prod_le_prod_of_subset_of_le_one`
`prod_le_one` 📖	mathematical	`Preorder.toLE` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass`	`Preorder.toLE` `prod` `CommMonoidWithZero.toCommMonoid` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero`	—	`prod_const_one` `prod_le_prod`
`prod_le_prod` 📖	mathematical	`Preorder.toLE` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero`	`Preorder.toLE` `prod` `CommMonoidWithZero.toCommMonoid`	—	`cons_induction` `instReflLe` `prod_cons` `posMulMono_iff_mulPosMono` `CommMagma.to_isCommutative` `mul_le_mul` `prod_nonneg` `LE.le.trans`
`prod_le_prod_of_subset_of_le_one` 📖	mathematical	`Finset` `instHasSubset` `Preorder.toLE` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass`	`Preorder.toLE` `prod` `CommMonoidWithZero.toCommMonoid`	—	`posMulMono_iff_mulPosMono` `CommMagma.to_isCommutative` `sdiff_union_of_subset` `prod_union` `sdiff_disjoint` `mul_le_of_le_one_left` `prod_nonneg` `prod_le_one`
`prod_le_prod_of_subset_of_one_le` 📖	mathematical	`Finset` `instHasSubset` `Preorder.toLE` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass`	`Preorder.toLE` `prod` `CommMonoidWithZero.toCommMonoid`	—	`posMulMono_iff_mulPosMono` `CommMagma.to_isCommutative` `le_mul_of_one_le_left` `prod_nonneg` `one_le_prod` `prod_union` `sdiff_disjoint` `sdiff_union_of_subset`
`prod_lt_prod` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `Preorder.toLE` `Finset` `SetLike.instMembership` `instSetLike`	`Preorder.toLT` `PartialOrder.toPreorder` `prod` `CommMonoidWithZero.toCommMonoid`	—	`insert_erase` `prod_insert` `notMem_erase` `posMulStrictMono_iff_mulPosStrictMono` `CommMagma.to_isCommutative` `mul_lt_mul_of_pos_of_nonneg'` `PosMulStrictMono.toPosMulMono` `prod_le_prod` `le_of_lt` `mem_of_mem_erase` `prod_pos` `LE.le.trans` `LT.lt.le`
`prod_lt_prod_of_nonempty` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `Nonempty`	`Preorder.toLT` `PartialOrder.toPreorder` `prod` `CommMonoidWithZero.toCommMonoid`	—	`prod_lt_prod` `le_of_lt`
`prod_mono_set_of_one_le` 📖	mathematical	`Preorder.toLE` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero`	`Monotone` `Finset` `PartialOrder.toPreorder` `partialOrder` `prod` `CommMonoidWithZero.toCommMonoid`	—	`prod_le_prod_of_subset_of_one_le` `LE.le.trans` `zero_le_one`
`prod_nonneg` 📖	mathematical	`Preorder.toLE` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero`	`Preorder.toLE` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `prod` `CommMonoidWithZero.toCommMonoid`	—	`prod_induction` `mul_nonneg` `zero_le_one`
`prod_pos` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero`	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `prod` `CommMonoidWithZero.toCommMonoid`	—	`prod_induction` `mul_pos` `zero_lt_one` `NeZero.one`

---

← Back to Index