Theorems · Definition · combinatorics
Tree
Deprecated since 2026-06-07Use BinaryTree instead.
Type u → Type u
Alias of BinaryTree.
A binary tree with values stored in non-leaf nodes.
- Defined in
- Mathlib.Data.Tree.Basic
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- BinaryTreeproof · cited by 41
Cited by14
Results whose statement or proof uses this declaration.
- Tree.treesOfNumNodesEqstatement · cited by 0
- Tree.unitRecOnstatement and proof · cited by 0
- Tree.getstatement and proof · cited by 0
- Tree.getOrElsestatement and proof · cited by 0
- Tree.heightstatement and proof · cited by 0
- Tree.indexOfstatement · cited by 0
- Tree.leftstatement and proof · cited by 0
- Tree.mapstatement and proof · cited by 0
- Tree.nilstatement · cited by 0
- Tree.nodestatement and proof · cited by 0
- Tree.numLeavesstatement and proof · cited by 0
- Tree.numNodesstatement and proof · cited by 0