Documentation Verification Report

Finset

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

Statistics

Metric	Count
Definitions `evalFinsetProd`	1
Theorems `map_prod`, `sum_le`, `prod_pos`, `coe_prod`, `abs_prod`, `le_prod_max_one`, `le_prod_of_submultiplicative_of_nonneg`, `le_prod_of_submultiplicative_on_pred_of_nonneg`, `prod_add_prod_le`, `prod_add_prod_le'`, `prod_le_one`, `prod_le_prod`, `prod_lt_prod`, `prod_lt_prod_of_nonempty`, `prod_nonneg`, `prod_pos`, `sq_sum_div_le_sum_sq_div`, `sum_mul_self_eq_zero_iff`, `sum_mul_sq_le_sq_mul_sq`, `sum_sq_le_sq_sum_of_nonneg`, `sum_sq_le_sum_mul_sum_of_sq_eq_mul`, `abv_sum`, `map_prod`, `prod_ne_zero`	24
Total	25

AbsoluteValue

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_prod` 📖	mathematical	—	`DFunLike.coe` `AbsoluteValue` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `funLike` `Finset.prod` `CommSemiring.toCommMonoid` `CommRing.toCommMonoid`	—	`map_prod` `MonoidWithZeroHomClass.toMonoidHomClass` `monoidWithZeroHomClass` `IsStrictOrderedRing.isDomain` `AddGroup.existsAddOfLE`
`sum_le` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `DFunLike.coe` `AbsoluteValue` `funLike` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`Finset.le_sum_of_subadditive` `IsOrderedRing.toIsOrderedAddMonoid` `Eq.le` `map_zero` `zeroHomClass` `add_le`

CanonicallyOrderedAdd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prod_pos` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Finset.prod` `CommSemiring.toCommMonoid`	—	`multiset_prod_pos` `Multiset.forall_mem_map_iff`

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abs_prod` 📖	mathematical	—	`abs` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `prod` `CommRing.toCommMonoid`	—	`map_prod` `MonoidWithZeroHomClass.toMonoidHomClass` `MonoidWithZeroHom.monoidWithZeroHomClass` `IsStrictOrderedRing.toIsOrderedRing`
`le_prod_max_one` 📖	mathematical	`Finset` `instMembership`	`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`
`le_prod_of_submultiplicative_of_nonneg` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `MulOne.toMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	`prod` `CommSemiring.toCommMonoid`	—	`le_trans` `Multiset.le_prod_of_submultiplicative_of_nonneg` `IsOrderedRing.toPosMulMono` `Multiset.map_map` `Multiset.map_congr`
`le_prod_of_submultiplicative_on_pred_of_nonneg` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `MulOne.toMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	`prod` `CommSemiring.toCommMonoid`	—	`le_trans` `Multiset.le_prod_of_submultiplicative_on_pred_of_nonneg` `IsOrderedRing.toPosMulMono` `Multiset.mem_map` `Multiset.map_map` `Multiset.map_congr`
`prod_add_prod_le` 📖	mathematical	`Finset` `instMembership` `Preorder.toLE` `PartialOrder.toPreorder` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	`prod` `CommSemiring.toCommMonoid`	—	`prod_eq_mul_prod_diff_singleton` `le_trans` `right_distrib` `Distrib.rightDistribClass` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `prod_le_prod` `IsOrderedRing.toZeroLEOneClass` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `prod_nonneg`
`prod_add_prod_le'` 📖	mathematical	`Finset` `instMembership` `Preorder.toLE` `PartialOrder.toPreorder` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	`prod` `CommSemiring.toCommMonoid`	—	`prod_eq_mul_prod_diff_singleton` `le_imp_le_of_le_of_le` `le_refl` `mul_le_mul_left` `covariant_swap_mul_of_covariant_mul` `CanonicallyOrderedAdd.toMulLeftMono` `right_distrib` `Distrib.rightDistribClass` `add_le_add` `CanonicallyOrderedAdd.toAddLeftMono` `covariant_swap_add_of_covariant_add` `mul_le_mul_right` `prod_le_prod` `CanonicallyOrderedAdd.toZeroLEOneClass` `MulLeftMono.toPosMulMono` `zero_le`
`prod_le_one` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass`	`prod` `CommMonoidWithZero.toCommMonoid`	—	`prod_const_one` `prod_le_prod`
`prod_le_prod` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero`	`prod` `CommMonoidWithZero.toCommMonoid`	—	`cons_induction` `prod_cons` `posMulMono_iff_mulPosMono` `CommMagma.to_isCommutative` `mul_le_mul` `prod_nonneg` `LE.le.trans`
`prod_lt_prod` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `Preorder.toLE` `Finset` `instMembership`	`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`	`prod` `CommMonoidWithZero.toCommMonoid`	—	`prod_lt_prod` `le_of_lt`
`prod_nonneg` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `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`	`prod` `CommMonoidWithZero.toCommMonoid`	—	`prod_induction` `mul_pos` `zero_lt_one` `NeZero.one`
`sq_sum_div_le_sum_sq_div` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring`	`Preorder.toLE` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid` `DivisionSemiring.toGroupWithZero` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `sum` `NonUnitalNonAssocSemiring.toAddCommMonoid`	—	`LT.lt.le` `div_nonneg` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `sq_nonneg` `IsOrderedRing.toPosMulMono` `IsStrictOrderedRing.toIsOrderedRing` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `div_le_of_le_mul₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `sum_nonneg` `sum_sq_le_sum_mul_sum_of_sq_eq_mul` `div_mul_cancel₀` `LT.lt.ne'`
`sum_mul_self_eq_zero_iff` 📖	mathematical	—	`sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`sum_eq_zero_iff_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `mul_self_nonneg` `IsOrderedRing.toPosMulMono` `IsStrictOrderedRing.noZeroDivisors`
`sum_mul_sq_le_sq_mul_sq` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`sum_sq_le_sum_mul_sum_of_sq_eq_mul` `sq_nonneg` `IsOrderedRing.toPosMulMono` `IsStrictOrderedRing.toIsOrderedRing` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `mul_pow`
`sum_sq_le_sq_sum_of_nonneg` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	`sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`sum_congr` `sq` `sum_mul_sum` `sum_le_sum` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `mul_sum` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `single_le_sum`
`sum_sq_le_sum_mul_sum_of_sq_eq_mul` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	`sum` `NonUnitalNonAssocSemiring.toAddCommMonoid`	—	`LE.le.eq_or_lt'` `sum_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `sum_eq_zero` `sum_eq_zero_iff_of_nonneg` `MulZeroClass.mul_zero` `isReduced_of_noZeroDivisors` `IsStrictOrderedRing.noZeroDivisors` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `zero_pow` `le_of_mul_le_mul_of_pos_left` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `le_of_add_le_add_left` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `IsCancelAdd.toIsLeftCancelAdd` `IsOrderedCancelAddMonoid.toIsCancelAdd` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `sum_congr` `mul_assoc` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.mul_pp_pf_overlap` `Mathlib.Tactic.Ring.mul_one` `sum_le_sum` `two_mul_le_add_of_sq_eq_mul` `IsStrictOrderedRing.toMulPosStrictMono` `mul_nonneg` `IsOrderedRing.toPosMulMono` `sq_nonneg` `sum_add_distrib` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_add_gt`

Finset.PNat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_prod` 📖	mathematical	—	`PNat.val` `Finset.prod` `PNat` `PNat.instCommMonoid` `Nat.instCommMonoid`	—	`map_prod` `MonoidHom.instMonoidHomClass`

IsAbsoluteValue

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abv_sum` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`AbsoluteValue.sum_le`
`map_prod` 📖	mathematical	—	`Finset.prod` `CommSemiring.toCommMonoid` `CommRing.toCommMonoid`	—	`AbsoluteValue.map_prod`

Mathlib.Meta.Positivity

Definitions

Name	Category	Theorems
`evalFinsetProd` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prod_ne_zero` 📖	—	—	—	—	`Finset.prod_ne_zero_iff`

---

← Back to Index