Stirling

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

Statistics

Metric	Count
Definitions `stirlingFirst`, `stirlingSecond`	2
Theorems `stirlingFirst_eq_zero_of_lt`, `stirlingFirst_one_right`, `stirlingFirst_self`, `stirlingFirst_succ_left`, `stirlingFirst_succ_right`, `stirlingFirst_succ_self_left`, `stirlingFirst_succ_succ`, `stirlingFirst_succ_zero`, `stirlingFirst_zero`, `stirlingFirst_zero_succ`, `stirlingSecond_eq_zero_of_lt`, `stirlingSecond_one_right`, `stirlingSecond_self`, `stirlingSecond_succ_left`, `stirlingSecond_succ_right`, `stirlingSecond_succ_self_left`, `stirlingSecond_succ_succ`, `stirlingSecond_succ_zero`, `stirlingSecond_zero`, `stirlingSecond_zero_succ`	20
Total	22

Nat

Definitions

Name	Category	Theorems
`stirlingFirst` 📖	CompOp	10 math math: `stirlingFirst_eq_zero_of_lt`, `stirlingFirst_succ_left`, `stirlingFirst_succ_right`, `stirlingFirst_zero_succ`, `stirlingFirst_one_right`, `stirlingFirst_succ_succ`, `stirlingFirst_succ_self_left`, `stirlingFirst_succ_zero`, `stirlingFirst_zero`, `stirlingFirst_self`
`stirlingSecond` 📖	CompOp	10 math math: `stirlingSecond_zero`, `stirlingSecond_succ_right`, `stirlingSecond_zero_succ`, `stirlingSecond_eq_zero_of_lt`, `stirlingSecond_one_right`, `stirlingSecond_succ_self_left`, `stirlingSecond_succ_zero`, `stirlingSecond_self`, `stirlingSecond_succ_left`, `stirlingSecond_succ_succ`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`stirlingFirst_eq_zero_of_lt` 📖	mathematical	—	`stirlingFirst`	—	`stirlingFirst.eq_2` `stirlingFirst_succ_succ` `MulZeroClass.mul_zero`
`stirlingFirst_one_right` 📖	mathematical	—	`stirlingFirst` `factorial`	—	`stirlingFirst_succ_succ` `zero_add` `stirlingFirst_succ_zero` `add_zero`
`stirlingFirst_self` 📖	mathematical	—	`stirlingFirst`	—	`stirlingFirst_eq_zero_of_lt` `MulZeroClass.mul_zero`
`stirlingFirst_succ_left` 📖	mathematical	—	`stirlingFirst`	—	—
`stirlingFirst_succ_right` 📖	mathematical	—	`stirlingFirst`	—	—
`stirlingFirst_succ_self_left` 📖	mathematical	—	`stirlingFirst` `choose`	—	`zero_add` `choose_succ_self` `stirlingFirst_succ_succ` `stirlingFirst_self` `mul_one` `choose_succ_succ` `choose_one_right`
`stirlingFirst_succ_succ` 📖	mathematical	—	`stirlingFirst`	—	—
`stirlingFirst_succ_zero` 📖	mathematical	—	`stirlingFirst`	—	—
`stirlingFirst_zero` 📖	mathematical	—	`stirlingFirst`	—	—
`stirlingFirst_zero_succ` 📖	mathematical	—	`stirlingFirst`	—	—
`stirlingSecond_eq_zero_of_lt` 📖	mathematical	—	`stirlingSecond`	—	`stirlingSecond.eq_2` `MulZeroClass.mul_zero`
`stirlingSecond_one_right` 📖	mathematical	—	`stirlingSecond`	—	`stirlingSecond.eq_4` `stirlingSecond_succ_zero`
`stirlingSecond_self` 📖	mathematical	—	`stirlingSecond`	—	`stirlingSecond_eq_zero_of_lt` `MulZeroClass.mul_zero`
`stirlingSecond_succ_left` 📖	mathematical	—	`stirlingSecond`	—	—
`stirlingSecond_succ_right` 📖	mathematical	—	`stirlingSecond`	—	—
`stirlingSecond_succ_self_left` 📖	mathematical	—	`stirlingSecond` `choose`	—	`zero_add` `choose_succ_self` `stirlingSecond_succ_succ` `stirlingSecond_self` `mul_one` `choose_succ_succ` `choose_one_right`
`stirlingSecond_succ_succ` 📖	mathematical	—	`stirlingSecond`	—	—
`stirlingSecond_succ_zero` 📖	mathematical	—	`stirlingSecond`	—	—
`stirlingSecond_zero` 📖	mathematical	—	`stirlingSecond`	—	—
`stirlingSecond_zero_succ` 📖	mathematical	—	`stirlingSecond`	—	—

---

← Back to Index