Catalan

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

Statistics

Metric	Count
Definitions pairwiseNode, treesOfNumNodesEq, catalan	3
Theorems coe_treesOfNumNodesEq, mem_treesOfNumNodesEq, mem_treesOfNumNodesEq_numNodes, treesOfNumNodesEq_card_eq_catalan, treesOfNumNodesEq_succ, treesOfNumNodesEq_zero, catalan_eq_centralBinom_div, catalan_one, catalan_succ, catalan_succ', catalan_three, catalan_two, catalan_zero, succ_mul_catalan_eq_centralBinom	14
Total	17

Tree

Definitions

Name	Category	Theorems
pairwiseNode 📖	CompOp	1 math math: treesOfNumNodesEq_succ
treesOfNumNodesEq 📖	CompOp	8 math math: treesOfNumNodesEq_succ, treesOfNumNodesEq_card_eq_catalan, DyckWord.equivTreesOfNumNodesEq_symm_apply_coe, DyckWord.equivTreesOfNumNodesEq_apply_coe, mem_treesOfNumNodesEq_numNodes, coe_treesOfNumNodesEq, mem_treesOfNumNodesEq, treesOfNumNodesEq_zero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_treesOfNumNodesEq 📖	mathematical	—	SetLike.coe Finset Tree Finset.instSetLike treesOfNumNodesEq setOf numNodes	—	Set.ext
mem_treesOfNumNodesEq 📖	mathematical	—	Tree Finset Finset.instMembership treesOfNumNodesEq numNodes	—	treesOfNumNodesEq_zero treesOfNumNodesEq_succ
mem_treesOfNumNodesEq_numNodes 📖	mathematical	—	Tree Finset Finset.instMembership treesOfNumNodesEq numNodes	—	mem_treesOfNumNodesEq
treesOfNumNodesEq_card_eq_catalan 📖	mathematical	—	Finset.card Tree treesOfNumNodesEq catalan	—	Nat.case_strong_induction_on treesOfNumNodesEq_zero Finset.card_singleton catalan_zero treesOfNumNodesEq_succ Finset.card_biUnion catalan_succ' Finset.sum_congr Finset.card_map Finset.card_product Finset.antidiagonal.fst_le Nat.instCanonicallyOrderedAdd Finset.antidiagonal.snd_le
treesOfNumNodesEq_succ 📖	mathematical	—	treesOfNumNodesEq Finset.biUnion Tree instDecidableEqTree Finset.HasAntidiagonal.antidiagonal Nat.instAddMonoid Finset.Nat.instHasAntidiagonal pairwiseNode	—	treesOfNumNodesEq.eq_2 Finset.ext
treesOfNumNodesEq_zero 📖	mathematical	—	treesOfNumNodesEq Tree Finset Finset.instSingleton nil	—	treesOfNumNodesEq.eq_1

(root)

Definitions

Name	Category	Theorems
catalan 📖	CompOp	11 math math: PowerSeries.catalanSeries_coeff, succ_mul_catalan_eq_centralBinom, Tree.treesOfNumNodesEq_card_eq_catalan, catalan_two, catalan_zero, catalan_succ, catalan_three, catalan_succ', DyckWord.card_dyckWord_semilength_eq_catalan, catalan_eq_centralBinom_div, catalan_one

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
catalan_eq_centralBinom_div 📖	mathematical	—	catalan Nat.centralBinom	—	catalan_zero Nat.cast_one Nat.centralBinom_zero Nat.cast_zero zero_add div_self NeZero.charZero_one Rat.instCharZero catalan_succ Nat.cast_sum Finset.sum_congr Nat.cast_mul tsub_le_self Nat.instCanonicallyOrderedAdd Nat.instOrderedSub mul_div Finset.sum_range Finset.sum_range_sub Nat.succ_dvd_centralBinom Int.cast_natCast Int.instCharZero
catalan_one 📖	mathematical	—	catalan	—	catalan_succ Finset.sum_congr Finset.univ_unique catalan_zero tsub_self Nat.instCanonicallyOrderedAdd Nat.instOrderedSub mul_one Finset.sum_const Finset.card_singleton
catalan_succ 📖	mathematical	—	catalan Finset.sum Nat.instAddCommMonoid Finset.univ Fin.fintype	—	catalan.eq_2
catalan_succ' 📖	mathematical	—	catalan Finset.sum Nat.instAddCommMonoid Finset.HasAntidiagonal.antidiagonal Nat.instAddMonoid Finset.Nat.instHasAntidiagonal	—	catalan_succ Finset.Nat.sum_antidiagonal_eq_sum_range_succ Finset.sum_range
catalan_three 📖	mathematical	—	catalan	—	catalan_eq_centralBinom_div add_zero Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.isNat_natDiv
catalan_two 📖	mathematical	—	catalan	—	catalan_eq_centralBinom_div add_zero Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.isNat_natDiv
catalan_zero 📖	mathematical	—	catalan	—	catalan.eq_1
succ_mul_catalan_eq_centralBinom 📖	mathematical	—	catalan Nat.centralBinom	—	Nat.succ_dvd_centralBinom catalan_eq_centralBinom_div

---

← Back to Index