Documentation Verification Report

BigOperators

📁 Source: Mathlib/Data/Finsupp/BigOperators.lean

Statistics

Metric	Count
Definitions	0
Theorems `mem_sup_support_iff`, `support_sum_eq`, `support_sum_subset`, `mem_foldr_sup_support_iff`, `support_sum_eq`, `support_sum_subset`, `mem_sup_map_support_iff`, `support_sum_eq`, `support_sum_subset`	9
Total	9

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_sup_support_iff` 📖	mathematical	—	`Finset` `instMembership` `sup` `Finsupp` `Lattice.toSemilatticeSup` `instLattice` `instOrderBot` `Finsupp.support`	—	`Multiset.mem_sup_map_support_iff`
`support_sum_eq` 📖	mathematical	`Set.PairwiseDisjoint` `Finset` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `partialOrder` `instOrderBot` `SetLike.coe` `instSetLike` `Finsupp.support`	`sum` `Finsupp.instAddCommMonoid` `sup` `Lattice.toSemilatticeSup` `instLattice`	—	`toList_toFinset` `nodup_toList` `List.toFinset_val` `List.dedup_eq_self` `Multiset.pairwise_coe_iff_pairwise` `symmetric_disjoint` `List.pairwiseDisjoint_iff_coe_toFinset_pairwise_disjoint` `sum_val` `Multiset.support_sum_eq`
`support_sum_subset` 📖	mathematical	—	`Finset` `instHasSubset` `Finsupp.support` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `sum` `Finsupp` `Finsupp.instAddCommMonoid` `sup` `Lattice.toSemilatticeSup` `instLattice` `instOrderBot`	—	`sum_congr` `sum_val` `Multiset.support_sum_subset`

List

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_foldr_sup_support_iff` 📖	mathematical	—	`Finset` `Finset.instMembership` `Finsupp` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `Finset.instLattice` `Finsupp.support` `Finset.instEmptyCollection`	—	—
`support_sum_eq` 📖	mathematical	`Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `Function.onFun` `Finset` `Disjoint` `Finset.partialOrder` `Finset.instOrderBot` `Finsupp.support`	`Finsupp.instAdd` `Finsupp.instZero` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `Finset.instLattice` `Finset.instEmptyCollection`	—	`Finsupp.support_add_eq` `Finset.bot_eq_empty` `foldr_sup_eq_sup_toFinset` `Finset.disjoint_sup_right` `Finset.disjoint_of_subset_right` `support_sum_subset` `Finset.sup_eq_union`
`support_sum_subset` 📖	mathematical	—	`Finset` `Finset.instHasSubset` `Finsupp.support` `AddZero.toZero` `AddZeroClass.toAddZero` `Finsupp` `Finsupp.instAdd` `Finsupp.instZero` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `Finset.instLattice` `Finset.instEmptyCollection`	—	`Finset.instReflSubset` `HasSubset.Subset.trans` `Finset.instIsTransSubset` `Finsupp.support_add` `Finset.union_subset_union` `Finset.Subset.rfl`

Multiset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_sup_map_support_iff` 📖	mathematical	—	`Finset` `Finset.instMembership` `sup` `Lattice.toSemilatticeSup` `Finset.instLattice` `Finset.instOrderBot` `map` `Finsupp` `Finsupp.support` `Multiset` `instMembership`	—	`List.mem_foldr_sup_support_iff`
`support_sum_eq` 📖	mathematical	`Pairwise` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Function.onFun` `Finset` `Disjoint` `Finset.partialOrder` `Finset.instOrderBot` `Finsupp.support`	`sum` `Finsupp.instAddCommMonoid` `sup` `Lattice.toSemilatticeSup` `Finset.instLattice` `map`	—	`Disjoint.symm` `List.support_sum_eq`
`support_sum_subset` 📖	mathematical	—	`Finset` `Finset.instHasSubset` `Finsupp.support` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `sum` `Finsupp` `Finsupp.instAddCommMonoid` `sup` `Lattice.toSemilatticeSup` `Finset.instLattice` `Finset.instOrderBot` `map`	—	`List.support_sum_subset`

---

← Back to Index