Documentation Verification Report

Bell

📁 Source: Mathlib/Combinatorics/Enumerative/Bell.lean

Statistics

Metric	Count
Definitions `bell`, `bell`, `uniformBell`	3
Theorems `bell_eq`, `bell_mul_eq`, `bell_zero`, `bell_one`, `bell_succ`, `bell_succ'`, `bell_two`, `bell_zero`, `uniformBell_eq`, `uniformBell_eq_div`, `uniformBell_mul_eq`, `uniformBell_one_left`, `uniformBell_one_right`, `uniformBell_succ_left`, `uniformBell_zero_left`, `uniformBell_zero_right`	16
Total	19

Multiset

Definitions

Name	Category	Theorems
`bell` 📖	CompOp	3 math math: `bell_zero`, `bell_mul_eq`, `bell_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bell_eq` 📖	mathematical	—	`bell` `Nat.factorial` `sum` `Nat.instAddCommMonoid` `prod` `Nat.instCommMonoid` `map` `Finset.prod` `Finset.erase` `toFinset` `count`	—	`Nat.instCanonicallyOrderedAdd` `IsStrictOrderedRing.noZeroDivisors` `Nat.instIsStrictOrderedRing` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instNontrivial` `Nat.factorial_pos` `Finset.prod_pos` `Nat.instZeroLEOneClass` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `bell_mul_eq` `mul_assoc`
`bell_mul_eq` 📖	mathematical	—	`bell` `prod` `Nat.instCommMonoid` `map` `Nat.factorial` `Finset.prod` `Finset.erase` `toFinset` `count` `sum` `Nat.instAddCommMonoid`	—	`ne_of_gt` `Finset.prod_pos` `Nat.instZeroLEOneClass` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `Nat.instNontrivial` `Nat.factorial_pos` `Nat.multinomial_spec` `mul_assoc` `mul_comm` `Finset.prod_mul_distrib` `Finset.prod_multiset_map_count` `Finset.prod_congr` `Finset.prod_erase_mul` `one_pow` `mul_one` `MulZeroClass.zero_mul` `Finset.erase_eq_of_notMem` `Finset.sum_multiset_count` `Finset.sum_congr`
`bell_zero` 📖	mathematical	—	`bell` `Multiset` `instZero`	—	—

Nat

Definitions

Name	Category	Theorems
`bell` 📖	CompOp	5 math math: `bell_zero`, `bell_succ'`, `bell_two`, `bell_succ`, `bell_one`
`uniformBell` 📖	CompOp	11 math math: `uniformBell_eq_div`, `DividedPowers.OfInvertibleFactorial.dpow_comp`, `uniformBell_mul_eq`, `DividedPowers.dpow_comp`, `uniformBell_one_right`, `uniformBell_eq`, `DividedPowers.OfInvertibleFactorial.dpow_comp_of_mul_lt`, `uniformBell_one_left`, `uniformBell_zero_right`, `uniformBell_zero_left`, `uniformBell_succ_left`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bell_one` 📖	mathematical	—	`bell`	—	`bell.eq_2` `Finset.sum_congr` `Finset.univ_unique` `choose_self` `tsub_self` `instCanonicallyOrderedAdd` `instOrderedSub` `bell_zero` `mul_one` `Finset.sum_const` `Finset.card_singleton`
`bell_succ` 📖	mathematical	—	`bell` `Finset.sum` `instAddCommMonoid` `Finset.univ` `Fin.fintype` `choose`	—	`bell.eq_2`
`bell_succ'` 📖	mathematical	—	`bell` `Finset.sum` `instAddCommMonoid` `Finset.HasAntidiagonal.antidiagonal` `instAddMonoid` `Finset.Nat.instHasAntidiagonal` `choose`	—	`bell_succ` `Finset.Nat.sum_antidiagonal_eq_sum_range_succ` `Finset.sum_range`
`bell_two` 📖	mathematical	—	`bell`	—	`bell.eq_2` `Finset.sum_congr` `Fin.sum_univ_two` `choose_succ_self_right` `zero_add` `tsub_zero` `instOrderedSub` `bell_one` `mul_one` `choose_self` `tsub_self` `instCanonicallyOrderedAdd` `bell_zero`
`bell_zero` 📖	mathematical	—	`bell`	—	—
`uniformBell_eq` 📖	mathematical	—	`uniformBell` `Finset.prod` `instCommMonoid` `Finset.range` `choose`	—	`Multiset.toFinset_replicate` `Finset.prod_congr` `Multiset.count.congr_simp` `Multiset.count_eq_zero_of_notMem` `MulZeroClass.mul_zero` `multinomial_empty` `Finset.erase_eq_of_notMem` `Finset.prod_const_one` `mul_one` `multinomial_singleton` `Finset.erase_singleton` `add_zero` `zero_tsub` `instCanonicallyOrderedAdd` `instOrderedSub` `choose_self` `Multiset.count_replicate` `mul_ite` `Finset.prod_singleton` `one_mul`
`uniformBell_eq_div` 📖	mathematical	—	`uniformBell` `factorial` `Monoid.toNatPow` `instMonoid`	—	`factorial_pos` `mul_assoc` `uniformBell_mul_eq`
`uniformBell_mul_eq` 📖	mathematical	—	`uniformBell` `Monoid.toNatPow` `instMonoid` `factorial`	—	`Multiset.map_replicate` `Multiset.prod_replicate` `Finset.prod_congr` `Multiset.toFinset_replicate` `factorial_zero` `Finset.prod_empty` `Finset.erase_eq_of_notMem` `Finset.prod_singleton` `Multiset.count_replicate_self` `Multiset.sum_replicate` `Multiset.bell_mul_eq`
`uniformBell_one_left` 📖	mathematical	—	`uniformBell`	—	`uniformBell_eq` `Finset.prod_singleton` `MulZeroClass.zero_mul` `zero_add` `choose_self`
`uniformBell_one_right` 📖	mathematical	—	`uniformBell`	—	`uniformBell_eq` `Finset.prod_congr` `mul_one` `add_tsub_cancel_right` `instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `tsub_eq_zero_of_le` `instCanonicallyOrderedAdd` `choose_zero_right` `Finset.prod_const_one`
`uniformBell_succ_left` 📖	mathematical	—	`uniformBell` `choose`	—	`uniformBell_eq` `Finset.prod_congr` `mul_comm` `Finset.prod_range_succ`
`uniformBell_zero_left` 📖	mathematical	—	`uniformBell`	—	`uniformBell_eq`
`uniformBell_zero_right` 📖	mathematical	—	`uniformBell`	—	`uniformBell_eq` `Finset.prod_congr` `MulZeroClass.mul_zero` `add_zero` `zero_tsub` `instCanonicallyOrderedAdd` `instOrderedSub` `choose_self` `Finset.prod_const_one`

---

← Back to Index