Commit 2023-03-17 12:26 2e567a95

View on Github →

chore: fix names in Combinatorics.Catalan (#2948) These were already wrong in mathlib3.

Estimated changes

Modified Mathlib/Combinatorics/Catalan.lean

deleted theorem Tree.coe_treesOfNodesEq

added theorem Tree.coe_treesOfNumNodesEq

deleted theorem Tree.mem_treesOfNodesEq

added theorem Tree.mem_treesOfNumNodesEq

added theorem Tree.mem_treesOfNumNodesEq_numNodes

deleted theorem Tree.mem_trees_of_nodes_eq_numNodes

deleted theorem Tree.treesOfNodesEq_card_eq_catalan

deleted theorem Tree.treesOfNodesEq_succ

deleted theorem Tree.treesOfNodesEq_zero

added theorem Tree.treesOfNumNodesEq_card_eq_catalan

added theorem Tree.treesOfNumNodesEq_succ

added theorem Tree.treesOfNumNodesEq_zero