Documentation Verification Report

Multiset

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

Statistics

Metric	Count
Definitions	0
Theorems `one_le_prod`, `one_le_prod_map`, `prod_map_le_pow_card`, `prod_map_le_prod_map₀`, `prod_map_lt_prod_map`, `prod_map_nonneg`, `prod_nonneg`, `prod_pos`	8
Total	8

Multiset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`one_le_prod` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero`	`prod` `CommMonoidWithZero.toCommMonoid`	—	`List.one_le_prod`
`one_le_prod_map` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero`	`prod` `CommMonoidWithZero.toCommMonoid` `map`	—	`one_le_prod` `mem_map`
`prod_map_le_pow_card` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `DFunLike.coe`	`prod` `CommMonoidWithZero.toCommMonoid` `map` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `card`	—	—
`prod_map_le_prod_map₀` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero`	`prod` `CommMonoidWithZero.toCommMonoid` `map`	—	`List.prod_map_le_prod_map₀`
`prod_map_lt_prod_map` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero`	`prod` `CommMonoidWithZero.toCommMonoid` `map`	—	`List.prod_map_lt_prod_map`
`prod_map_nonneg` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero`	`prod` `CommMonoidWithZero.toCommMonoid` `map`	—	`prod_nonneg` `mem_map`
`prod_nonneg` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero`	`prod` `CommMonoidWithZero.toCommMonoid`	—	`List.prod_nonneg`
`prod_pos` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero`	`prod` `CommMonoidWithZero.toCommMonoid`	—	`List.prod_pos`

---

← Back to Index