Documentation Verification Report

Multinomial

📁 Source: Mathlib/Data/Nat/Choose/Multinomial.lean

Statistics

Metric	Count
Definitions `multinomial`, `multinomial`, `multinomial`	3
Theorems `sum_pow`, `sum_pow_eq_sum_piAntidiag`, `sum_pow_eq_sum_piAntidiag_of_commute`, `sum_pow_of_commute`, `multinomial_eq`, `multinomial_eq_of_support_subset`, `multinomial_update`, `multinomial_filter_ne`, `multinomial_zero`, `binomial_eq`, `binomial_eq_choose`, `binomial_one`, `binomial_spec`, `binomial_succ_succ`, `multinomial_congr`, `multinomial_cons`, `multinomial_empty`, `multinomial_insert`, `multinomial_insert_one`, `multinomial_pos`, `multinomial_singleton`, `multinomial_spec`, `multinomial_two_mul_le_mul_multinomial`, `multinomial_univ_three`, `multinomial_univ_two`, `succ_mul_binomial`, `multinomial_coe_fill_of_notMem`	27
Total	30

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sum_pow` 📖	mathematical	—	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Sym` `sym` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Multiset.multinomial` `Multiset` `Multiset.card` `Multiset.prod` `CommSemiring.toCommMonoid` `Multiset.map`	—	`sum_coe_sort` `Multiset.map_set_pairwise` `Set.Pairwise.mono` `mem_sym_iff` `Commute.all` `sum_congr` `Multiset.noncommProd_eq_prod` `sum_pow_of_commute`
`sum_pow_eq_sum_piAntidiag` 📖	mathematical	—	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `piAntidiag` `Nat.instAddCommMonoid` `Nat.instHasAntidiagonal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Nat.multinomial` `prod` `CommSemiring.toCommMonoid`	—	`Commute.all` `sum_congr` `Set.Pairwise.mono'` `Commute.pow_pow` `sum_pow_eq_sum_piAntidiag_of_commute`
`sum_pow_eq_sum_piAntidiag_of_commute` 📖	mathematical	`Set.Pairwise` `SetLike.coe` `Finset` `instSetLike` `Function.onFun` `Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	`Monoid.toNatPow` `sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `piAntidiag` `Nat.instAddCommMonoid` `Nat.instHasAntidiagonal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Nat.multinomial` `noncommProd` `Set.Pairwise.mono'` `Commute.pow_pow`	—	`cons_induction` `Set.Pairwise.mono'` `Commute.pow_pow` `pow_zero` `sum_congr` `piAntidiag_zero` `Nat.instCanonicallyOrderedAdd` `Nat.multinomial_empty` `Nat.cast_one` `mul_one` `sum_const` `card_singleton` `nsmul_eq_mul` `zero_pow` `piAntidiag_empty_of_ne_zero` `zero_nsmul` `sum_cons` `Pi.instIsRightCancelAdd` `AddRightCancelSemigroup.toIsRightCancelAdd` `pairwiseDisjoint_piAntidiag_map_addRightEmbedding` `piAntidiag_cons` `sum_disjiUnion` `Set.Pairwise.mono` `mem_cons` `Nat.multinomial_cons` `Nat.cast_mul` `noncommProd_cons` `sum_map` `sum_add_distrib` `sum_ite_eq'` `add_zero` `noncommProd_congr` `cons_eq_insert` `coe_insert` `not_imp_comm` `mem_piAntidiag` `zero_add` `HasAntidiagonal.mem_antidiagonal` `Nat.multinomial_congr` `Pi.add_apply` `Commute.add_pow` `Commute.sum_right` `mul_sum` `sum_mul` `Nat.cast_comm` `Commute.left_comm` `Nat.commute_cast` `mul_assoc`
`sum_pow_of_commute` 📖	mathematical	`Set.Pairwise` `SetLike.coe` `Finset` `instSetLike` `Function.onFun` `Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	`Monoid.toNatPow` `sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Sym` `SetLike.instMembership` `sym` `univ` `Subtype.fintype` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Multiset.multinomial` `Multiset` `Multiset.card` `Multiset.noncommProd` `Multiset.map` `Multiset.map_set_pairwise` `Set.Pairwise.mono` `Multiset.instMembership` `val` `setOf` `instMembership` `mem_sym_iff`	—	`induction` `Multiset.map_set_pairwise` `Set.Pairwise.mono` `mem_sym_iff` `sum_empty` `pow_zero` `Unique.instSubsingleton` `Fintype.sum_subsingleton` `instSubsingletonSubtype_mathlib` `Multiset.multinomial_zero` `Nat.cast_one` `one_mul` `pow_succ` `MulZeroClass.mul_zero` `Fintype.sum_empty` `instIsEmpty` `sum_insert` `Commute.add_pow` `Commute.sum_right` `mem_insert_self` `mem_insert_of_mem` `sum_range` `subset_insert` `sum_congr` `mul_sum` `sum_mul` `sum_sigma'` `Fintype.sum_equiv` `Multiset.multinomial_filter_ne` `Multiset.filter_add_not` `Multiset.map_add` `Multiset.noncommProd.congr_simp` `Multiset.subset_of_le` `Multiset.le_add_right` `Multiset.le_add_left` `Multiset.noncommProd_add` `Multiset.map_congr` `Multiset.filter_eq` `Multiset.map_replicate` `Multiset.noncommProd_eq_pow_card` `Multiset.eq_of_mem_replicate` `Multiset.card_replicate` `Nat.cast_mul` `mul_assoc` `Nat.cast_comm`

Finsupp

Definitions

Name	Category	Theorems
`multinomial` 📖	CompOp	3 math math: `multinomial_eq_of_support_subset`, `multinomial_update`, `multinomial_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`multinomial_eq` 📖	mathematical	—	`multinomial` `Nat.multinomial` `support` `MulZeroClass.toZero` `Nat.instMulZeroClass` `DFunLike.coe` `Finsupp` `instFunLike`	—	—
`multinomial_eq_of_support_subset` 📖	mathematical	`Finset` `Finset.instHasSubset` `support` `MulZeroClass.toZero` `Nat.instMulZeroClass`	`multinomial` `Nat.multinomial` `DFunLike.coe` `Finsupp` `instFunLike`	—	`Finset.sum_subset` `Finset.prod_subset`
`multinomial_update` 📖	mathematical	—	`multinomial` `Nat.choose` `sum` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Nat.instAddCommMonoid` `DFunLike.coe` `Finsupp` `instFunLike` `update`	—	`Finset.insert_erase` `Nat.multinomial_insert` `Finset.notMem_erase` `Finset.add_sum_erase` `support_update_zero` `Nat.multinomial_congr` `Function.update_of_ne` `Finset.mem_erase` `notMem_support_iff` `Nat.choose_zero_right` `one_mul` `update_self`

Multiset

Definitions

Name	Category	Theorems
`multinomial` 📖	CompOp	7 math math: `multinomial_filter_ne`, `norm_iteratedFDerivWithin_prod_le`, `Finset.sum_pow_of_commute`, `multinomial_zero`, `norm_iteratedFDeriv_prod_le`, `Sym.multinomial_coe_fill_of_notMem`, `Finset.sum_pow`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`multinomial_filter_ne` 📖	mathematical	—	`multinomial` `Nat.choose` `card` `count` `filter`	—	`Finsupp.card_toMultiset` `toFinsupp_toMultiset` `Finsupp.ext` `toFinsupp_apply` `count_filter` `Finsupp.coe_update` `Function.update_of_ne` `not_ne_iff` `Function.update_self` `Finsupp.multinomial_update`
`multinomial_zero` 📖	mathematical	—	`multinomial` `Multiset` `instZero`	—	`map_zero` `AddMonoidHomClass.toZeroHomClass` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass` `Nat.instZeroLEOneClass`

Nat

Definitions

Name	Category	Theorems
`multinomial` 📖	CompOp	22 math math: `Finset.sum_pow_eq_sum_piAntidiag`, `binomial_succ_succ`, `multinomial_univ_two`, `Finsupp.multinomial_eq_of_support_subset`, `binomial_one`, `multinomial_spec`, `Finsupp.multinomial_eq`, `Finset.sum_pow_eq_sum_piAntidiag_of_commute`, `multinomial_cons`, `multinomial_insert_one`, `multinomial_two_mul_le_mul_multinomial`, `multinomial_singleton`, `multinomial_congr`, `multinomial_insert`, `multinomial_empty`, `binomial_spec`, `DividedPowers.prod_dpow`, `succ_mul_binomial`, `binomial_eq_choose`, `binomial_eq`, `multinomial_pos`, `multinomial_univ_three`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`binomial_eq` 📖	mathematical	—	`multinomial` `Finset` `Finset.instInsert` `Finset.instSingleton` `factorial`	—	`Finset.sum_pair` `Finset.prod_pair`
`binomial_eq_choose` 📖	mathematical	—	`multinomial` `Finset` `Finset.instInsert` `Finset.instSingleton` `choose`	—	`binomial_eq` `choose_eq_factorial_div_factorial` `add_tsub_cancel_left` `instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid`
`binomial_one` 📖	mathematical	—	`multinomial` `Finset` `Finset.instInsert` `Finset.instSingleton`	—	`multinomial_insert_one` `Finset.sum_singleton` `multinomial_singleton` `mul_one`
`binomial_spec` 📖	mathematical	—	`factorial` `multinomial` `Finset` `Finset.instInsert` `Finset.instSingleton`	—	`Finset.prod_pair` `Finset.sum_pair` `multinomial_spec`
`binomial_succ_succ` 📖	mathematical	—	`multinomial` `Finset` `Finset.instInsert` `Finset.instSingleton` `Function.update`	—	`binomial_eq_choose` `Function.update_apply` `choose_succ_succ` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero`
`multinomial_congr` 📖	mathematical	—	`multinomial`	—	`Finset.sum_congr` `Finset.prod_congr`
`multinomial_cons` 📖	mathematical	`Finset` `Finset.instMembership`	`multinomial` `Finset.cons` `choose` `Finset.sum` `instAddCommMonoid`	—	`multinomial.eq_1` `Finset.prod_pos` `instZeroLEOneClass` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `instNontrivial` `factorial_pos` `prod_factorial_dvd_factorial_sum` `Finset.prod_cons` `mul_assoc` `mul_left_comm` `choose_symm_add` `add_choose_mul_factorial_mul_factorial` `Finset.sum_cons`
`multinomial_empty` 📖	mathematical	—	`multinomial` `Finset` `Finset.instEmptyCollection`	—	`instZeroLEOneClass`
`multinomial_insert` 📖	mathematical	`Finset` `Finset.instMembership`	`multinomial` `Finset.instInsert` `choose` `Finset.sum` `instAddCommMonoid`	—	`Finset.cons_eq_insert` `multinomial_cons`
`multinomial_insert_one` 📖	mathematical	`Finset` `Finset.instMembership`	`multinomial` `Finset.instInsert` `Finset.sum` `instAddCommMonoid`	—	`Finset.sum_insert` `Finset.prod_insert` `add_comm` `factorial_succ` `zero_add` `mul_one` `one_mul` `prod_factorial_dvd_factorial_sum`
`multinomial_pos` 📖	mathematical	—	`multinomial`	—	`factorial_pos` `prod_factorial_dvd_factorial_sum` `prod_factorial_pos`
`multinomial_singleton` 📖	mathematical	—	`multinomial` `Finset` `Finset.instSingleton`	—	`Finset.notMem_empty` `Finset.cons_empty` `multinomial_cons` `add_zero` `choose_self` `multinomial_empty` `mul_one`
`multinomial_spec` 📖	mathematical	—	`Finset.prod` `instCommMonoid` `factorial` `multinomial` `Finset.sum` `instAddCommMonoid`	—	`prod_factorial_dvd_factorial_sum`
`multinomial_two_mul_le_mul_multinomial` 📖	mathematical	—	`multinomial` `Monoid.toNatPow` `instMonoid` `Finset.sum` `instAddCommMonoid`	—	`multinomial.eq_1` `Finset.mul_sum` `prod_factorial_dvd_factorial_sum` `ne_of_gt` `Finset.prod_pos` `instZeroLEOneClass` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `instNontrivial` `factorial_pos` `Dvd.dvd.trans` `mul_le_mul_left` `covariant_swap_mul_of_covariant_mul` `instMulLeftMono` `factorial_two_mul_le` `mul_pow` `Finset.prod_pow_eq_pow_sum` `Finset.prod_mul_distrib` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.mul_pf_right` `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` `mul_le_mul_right` `Finset.prod_le_prod` `IsOrderedRing.toPosMulMono` `IsStrictOrderedRing.toIsOrderedRing` `instIsStrictOrderedRing` `le_of_lt` `mul_pos` `pow_pos` `IsStrictOrderedRing.toPosMulStrictMono` `IsStrictOrderedRing.toZeroLEOneClass` `Mathlib.Meta.Positivity.pos_of_isNat` `Mathlib.Meta.NormNum.isNat_ofNat` `doubleFactorial_two_mul` `doubleFactorial_le_factorial`
`multinomial_univ_three` 📖	mathematical	—	`multinomial` `Finset.univ` `Fin.fintype` `Matrix.vecCons` `Matrix.vecEmpty` `factorial`	—	`multinomial.eq_1` `Fin.sum_univ_three` `Fin.prod_univ_three`
`multinomial_univ_two` 📖	mathematical	—	`multinomial` `Finset.univ` `Fin.fintype` `Matrix.vecCons` `Matrix.vecEmpty` `factorial`	—	`multinomial.eq_1` `Fin.sum_univ_two` `Fin.prod_univ_two`
`succ_mul_binomial` 📖	mathematical	—	`multinomial` `Finset` `Finset.instInsert` `Finset.instSingleton` `Function.update`	—	`binomial_eq_choose` `mul_comm` `Function.update_self` `Function.update_of_ne` `add_one_mul_choose_eq`

Sym

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`multinomial_coe_fill_of_notMem` 📖	mathematical	`Sym` `instMembership`	`Multiset.multinomial` `toMultiset` `fill` `Nat.choose`	—	`Multiset.multinomial_filter_ne` `card_coe` `count_coe_fill_self_of_notMem` `mem_coe` `coe_fill` `coe_replicate` `Multiset.filter_add` `Multiset.filter_eq_self` `add_eq_left` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `Multiset.filter_eq_nil` `Multiset.mem_replicate`

---

← Back to Index