Documentation Verification Report

Basic

📁 Source: Mathlib/Combinatorics/Enumerative/Partition/Basic.lean

Statistics

Metric	Count
Definitions `UniquePartitionOne`, `UniquePartitionZero`, `countRestricted`, `distincts`, `indiscrete`, `instFintype`, `instInhabited`, `oddDistincts`, `odds`, `ofComposition`, `ofMultiset`, `ofSums`, `ofSym`, `ofSymShapeEquiv`, `parts`, `restricted`, `toFinsuppAntidiag`, `instDecidableEqPartition`, `decEq`	19
Theorems `countRestricted_two`, `count_ofSums_of_ne_zero`, `count_ofSums_zero`, `ext`, `ext_iff`, `indiscrete_parts`, `le_of_mem_parts`, `ofComposition_parts`, `ofComposition_surj`, `ofMultiset_parts`, `ofSums_parts`, `ofSym_map`, `ofSym_one`, `partition_one_parts`, `partition_zero_parts`, `parts_pos`, `parts_sum`, `toFinsuppAntidiag_injective`, `toFinsuppAntidiag_mem_finsuppAntidiag`	19
Total	38

Nat

Definitions

Name	Category	Theorems
`instDecidableEqPartition` 📖	CompOp	—

Nat.Partition

Definitions

Name	Category	Theorems
`UniquePartitionOne` 📖	CompOp	—
`UniquePartitionZero` 📖	CompOp	—
`countRestricted` 📖	CompOp	5 math math: `card_restricted_eq_card_countRestricted`, `hasProd_powerSeriesMk_card_countRestricted`, `countRestricted_two`, `powerSeriesMk_card_restricted_eq_powerSeriesMk_card_countRestricted`, `powerSeriesMk_card_countRestricted_eq_tprod`
`distincts` 📖	CompOp	2 math math: `countRestricted_two`, `card_odds_eq_card_distincts`
`indiscrete` 📖	CompOp	10 math math: `indiscrete_parts`, `MvPolynomial.hsymmPart_indiscrete`, `MvPolynomial.psumPart_indiscrete`, `MvPolynomial.psumPart_zero`, `MvPolynomial.msymm_zero`, `MvPolynomial.hsymmPart_zero`, `MvPolynomial.esymmPart_zero`, `MvPolynomial.msymm_one`, `ofSym_one`, `MvPolynomial.esymmPart_indiscrete`
`instFintype` 📖	CompOp	1 math math: `coeff_genFun`
`instInhabited` 📖	CompOp	—
`oddDistincts` 📖	CompOp	—
`odds` 📖	CompOp	1 math math: `card_odds_eq_card_distincts`
`ofComposition` 📖	CompOp	2 math math: `ofComposition_parts`, `ofComposition_surj`
`ofMultiset` 📖	CompOp	1 math math: `ofMultiset_parts`
`ofSums` 📖	CompOp	3 math math: `ofSums_parts`, `count_ofSums_zero`, `count_ofSums_of_ne_zero`
`ofSym` 📖	CompOp	2 math math: `ofSym_map`, `ofSym_one`
`ofSymShapeEquiv` 📖	CompOp	—
`parts` 📖	CompOp	13 math math: `indiscrete_parts`, `ofMultiset_parts`, `ofComposition_parts`, `partition_zero_parts`, `partition_one_parts`, `ofSums_parts`, `count_ofSums_zero`, `Equiv.Perm.filter_parts_partition_eq_cycleType`, `count_ofSums_of_ne_zero`, `Equiv.Perm.parts_partition`, `ext_iff`, `parts_sum`, `coeff_genFun`
`restricted` 📖	CompOp	4 math math: `card_restricted_eq_card_countRestricted`, `powerSeriesMk_card_restricted_eq_tprod`, `powerSeriesMk_card_restricted_eq_powerSeriesMk_card_countRestricted`, `hasProd_powerSeriesMk_card_restricted`
`toFinsuppAntidiag` 📖	CompOp	2 math math: `toFinsuppAntidiag_mem_finsuppAntidiag`, `toFinsuppAntidiag_injective`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`countRestricted_two` 📖	mathematical	—	`countRestricted` `distincts`	—	`Multiset.nodup_iff_count_le_one`
`count_ofSums_of_ne_zero` 📖	mathematical	`Multiset.sum` `Nat.instAddCommMonoid`	`Multiset.count` `parts` `ofSums`	—	`Multiset.count_filter_of_pos`
`count_ofSums_zero` 📖	mathematical	`Multiset.sum` `Nat.instAddCommMonoid`	`Multiset.count` `parts` `ofSums`	—	`Multiset.count_filter_of_neg`
`ext` 📖	—	`parts`	—	—	—
`ext_iff` 📖	mathematical	—	`parts`	—	`ext`
`indiscrete_parts` 📖	mathematical	—	`parts` `indiscrete` `Multiset` `Multiset.instSingleton`	—	`Multiset.filter_congr`
`le_of_mem_parts` 📖	—	`Multiset` `Multiset.instMembership` `parts`	—	—	`parts_sum` `Multiset.le_sum_of_mem` `Nat.instCanonicallyOrderedAdd`
`ofComposition_parts` 📖	mathematical	—	`parts` `ofComposition` `Multiset.ofList` `Composition.blocks`	—	—
`ofComposition_surj` 📖	mathematical	—	`Composition` `Nat.Partition` `ofComposition`	—	`ext`
`ofMultiset_parts` 📖	mathematical	—	`parts` `Multiset.sum` `Nat.instAddCommMonoid` `ofMultiset` `Multiset.filter`	—	—
`ofSums_parts` 📖	mathematical	`Multiset.sum` `Nat.instAddCommMonoid`	`parts` `ofSums` `Multiset.filter`	—	—
`ofSym_map` 📖	mathematical	—	`ofSym` `Sym.map` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`Multiset.map_congr` `Multiset.dedup_map_of_injective` `Equiv.injective` `Multiset.map_map` `Multiset.count_map_eq_count'`
`ofSym_one` 📖	mathematical	—	`ofSym` `indiscrete`	—	`ext` `Multiset.ext'` `Multiset.count.congr_simp` `partition_one_parts`
`partition_one_parts` 📖	mathematical	—	`parts` `Multiset` `Multiset.instSingleton`	—	`Multiset.eq_replicate_card` `LE.le.antisymm` `LE.le.trans_eq` `Multiset.le_sum_of_mem` `Nat.instCanonicallyOrderedAdd` `parts_sum` `parts_pos` `Multiset.sum_replicate` `mul_one` `Multiset.replicate_one`
`partition_zero_parts` 📖	mathematical	—	`parts` `Multiset` `Multiset.instZero`	—	`Multiset.eq_zero_of_forall_notMem` `LT.lt.ne'` `parts_pos` `Multiset.sum_eq_zero_iff` `Nat.instCanonicallyOrderedAdd` `Nat.instIsOrderedAddMonoid` `parts_sum`
`parts_pos` 📖	—	`Multiset` `Multiset.instMembership` `parts`	—	—	—
`parts_sum` 📖	mathematical	—	`Multiset.sum` `Nat.instAddCommMonoid` `parts`	—	—
`toFinsuppAntidiag_injective` 📖	mathematical	—	`Nat.Partition` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `toFinsuppAntidiag`	—	`ext_iff` `Multiset.ext`
`toFinsuppAntidiag_mem_finsuppAntidiag` 📖	mathematical	—	`Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finset` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `Finset.instMembership` `Finset.finsuppAntidiag` `Finset.Nat.instHasAntidiagonal` `Finset.Icc` `Nat.instPreorder` `Nat.instLocallyFiniteOrder` `toFinsuppAntidiag`	—	`Finset.sum_multiset_count` `Finset.sum_subset` `IsDomain.to_noZeroDivisors` `Nat.instIsDomain` `parts_sum` `Finset.sum_congr`

Nat.instDecidableEqPartition

Definitions

Name	Category	Theorems
`decEq` 📖	CompOp	—

---

← Back to Index