Rooted Trees

This file defines planar rooted trees together with the equivalence relation generated by permuting the children at each vertex. The quotient by this relation is the type of non-planar rooted trees.

The type RootedTree contains non-empty rooted trees. The empty tree used in B-series indexing is adjoined separately as TreeIndex.empty.

Main definitions

• PTree - non-empty planar rooted trees
• PTree.Perm - equivalence relation forgetting the planar embedding
• RootedTree - non-empty non-planar rooted trees
• TreeIndex - rooted trees with an adjoined empty tree

References

• John C. Butcher, Numerical Methods for Ordinary Differential Equations
• Philippe Chartier, Ernst Hairer, Gilles Vilmart, Algebraic Structures of B-series

inductive HopfAlgebras.PTree : Type

Non-empty planar rooted trees, where the list of children at each node is ordered.

• node : List PTree → PTree

@[implicit_reducible]

instance HopfAlgebras.instReprPTree : Repr PTree

Equations

• HopfAlgebras.instReprPTree = { reprPrec := HopfAlgebras.instReprPTree.repr }

partial def HopfAlgebras.instReprPTree.repr : PTree → ℕ → Std.Format

inductive HopfAlgebras.PTree.Perm : PTree → PTree → Prop

t1.Perm t2 means that t1 and t2 differ only by permuting the children at each vertex, recursively.

• node {ts1 ts2 ts1' : List PTree} : ts1.Perm ts1' → List.Forall₂ Perm ts1' ts2 → (PTree.node ts1).Perm (PTree.node ts2)

def HopfAlgebras.PTree.bullet : PTree

The one-vertex planar rooted tree.

Equations

• HopfAlgebras.PTree.bullet = HopfAlgebras.PTree.node []

def HopfAlgebras.PTree.chain2 : PTree

A two-vertex planar rooted tree.

Equations

• HopfAlgebras.PTree.chain2 = HopfAlgebras.PTree.node [HopfAlgebras.PTree.bullet]

def HopfAlgebras.PTree.chain3 : PTree

A three-vertex planar chain.

Equations

• HopfAlgebras.PTree.chain3 = HopfAlgebras.PTree.node [HopfAlgebras.PTree.chain2]

def HopfAlgebras.PTree.cherry : PTree

A root with two bullet children.

Equations

• HopfAlgebras.PTree.cherry = HopfAlgebras.PTree.node [HopfAlgebras.PTree.bullet, HopfAlgebras.PTree.bullet]

def HopfAlgebras.PTree.order : PTree → ℕ

The number of vertices of a planar rooted tree.

Equations

• (HopfAlgebras.PTree.node a).order = 1 + HopfAlgebras.PTree.orderList a

def HopfAlgebras.PTree.orderList : List PTree → ℕ

The sum of the orders of a list of planar rooted trees.

Equations

• HopfAlgebras.PTree.orderList [] = 0
• HopfAlgebras.PTree.orderList (t :: ts) = t.order + HopfAlgebras.PTree.orderList ts

@[simp]

theorem HopfAlgebras.PTree.order_node (ts : List PTree) : (node ts).order = 1 + orderList ts

@[simp]

theorem HopfAlgebras.PTree.order_bullet : bullet.order = 1

@[simp]

theorem HopfAlgebras.PTree.order_chain2 : chain2.order = 2

@[simp]

theorem HopfAlgebras.PTree.order_chain3 : chain3.order = 3

@[simp]

theorem HopfAlgebras.PTree.order_cherry : cherry.order = 3

@[simp]

theorem HopfAlgebras.PTree.orderList_nil : orderList [] = 0

@[simp]

theorem HopfAlgebras.PTree.orderList_cons (t : PTree) (ts : List PTree) : orderList (t :: ts) = t.order + orderList ts

@[simp]

theorem HopfAlgebras.PTree.orderList_append (ts us : List PTree) : orderList (ts ++ us) = orderList ts + orderList us

theorem HopfAlgebras.PTree.order_pos (t : PTree) : 0 < t.order

@[simp]

theorem HopfAlgebras.PTree.orderList_reverse (ts : List PTree) : orderList ts.reverse = orderList ts

def HopfAlgebras.PTree.children : PTree → List PTree

The ordered list of subtrees at the root.

Equations

• (HopfAlgebras.PTree.node a).children = a

@[simp]

theorem HopfAlgebras.PTree.children_node (ts : List PTree) : (node ts).children = ts

@[simp]

theorem HopfAlgebras.PTree.node_children (t : PTree) : node t.children = t

theorem HopfAlgebras.PTree.order_eq_one_add_orderList_children (t : PTree) : t.order = 1 + orderList t.children

@[simp]

theorem HopfAlgebras.PTree.orderList_eq_zero_iff (ts : List PTree) : orderList ts = 0 ↔ ts = []

theorem HopfAlgebras.PTree.order_eq_one_iff (t : PTree) : t.order = 1 ↔ t = bullet

@[simp]

theorem HopfAlgebras.PTree.orderList_eq_one_iff (ts : List PTree) : orderList ts = 1 ↔ ts = [bullet]

theorem HopfAlgebras.PTree.order_eq_two_iff (t : PTree) : t.order = 2 ↔ t = chain2

theorem HopfAlgebras.PTree.orderList_eq_two_iff (ts : List PTree) : orderList ts = 2 ↔ ts = [chain2] ∨ ts = [bullet, bullet]

theorem HopfAlgebras.PTree.order_eq_three_iff (t : PTree) : t.order = 3 ↔ t = chain3 ∨ t = cherry

def HopfAlgebras.PTree.treeFactorial : PTree → ℕ

Butcher's tree factorial.

Equations

• (HopfAlgebras.PTree.node a).treeFactorial = (HopfAlgebras.PTree.node a).order * HopfAlgebras.PTree.treeFactorialList a

def HopfAlgebras.PTree.treeFactorialList : List PTree → ℕ

The product of tree factorials over a list of planar rooted trees.

Equations

• HopfAlgebras.PTree.treeFactorialList [] = 1
• HopfAlgebras.PTree.treeFactorialList (t :: ts) = t.treeFactorial * HopfAlgebras.PTree.treeFactorialList ts

@[simp]

theorem HopfAlgebras.PTree.treeFactorial_node (ts : List PTree) : (node ts).treeFactorial = (node ts).order * treeFactorialList ts

@[simp]

theorem HopfAlgebras.PTree.treeFactorial_bullet : bullet.treeFactorial = 1

@[simp]

theorem HopfAlgebras.PTree.treeFactorial_chain2 : chain2.treeFactorial = 2

@[simp]

theorem HopfAlgebras.PTree.treeFactorial_chain3 : chain3.treeFactorial = 6

@[simp]

theorem HopfAlgebras.PTree.treeFactorial_cherry : cherry.treeFactorial = 3

@[simp]

theorem HopfAlgebras.PTree.treeFactorialList_nil : treeFactorialList [] = 1

@[simp]

theorem HopfAlgebras.PTree.treeFactorialList_cons (t : PTree) (ts : List PTree) : treeFactorialList (t :: ts) = t.treeFactorial * treeFactorialList ts

theorem HopfAlgebras.PTree.treeFactorial_pos (t : PTree) : 0 < t.treeFactorial

theorem HopfAlgebras.PTree.treeFactorialList_pos (ts : List PTree) : 0 < treeFactorialList ts

theorem HopfAlgebras.PTree.treeFactorial_ne_zero (t : PTree) : t.treeFactorial ≠ 0

theorem HopfAlgebras.PTree.treeFactorialList_ne_zero (ts : List PTree) : treeFactorialList ts ≠ 0

@[simp]

theorem HopfAlgebras.PTree.treeFactorialList_append (ts us : List PTree) : treeFactorialList (ts ++ us) = treeFactorialList ts * treeFactorialList us

def HopfAlgebras.PTree.butcherProduct (ts : List PTree) : PTree → PTree

Attach an ordered forest as the first children of the root of a planar tree.

Equations

• HopfAlgebras.PTree.butcherProduct ts (HopfAlgebras.PTree.node a) = HopfAlgebras.PTree.node (ts ++ a)

@[simp]

theorem HopfAlgebras.PTree.butcherProduct_node (ts us : List PTree) : butcherProduct ts (node us) = node (ts ++ us)

@[simp]

theorem HopfAlgebras.PTree.butcherProduct_nil (t : PTree) : butcherProduct [] t = t

@[simp]

theorem HopfAlgebras.PTree.butcherProduct_bullet (ts : List PTree) : butcherProduct ts bullet = node ts

@[simp]

theorem HopfAlgebras.PTree.order_butcherProduct (ts : List PTree) (t : PTree) : (butcherProduct ts t).order = orderList ts + t.order

@[simp]

theorem HopfAlgebras.PTree.butcherProduct_assoc (ts us : List PTree) (t : PTree) : butcherProduct ts (butcherProduct us t) = butcherProduct (ts ++ us) t

theorem HopfAlgebras.PTree.treeFactorial_butcherProduct (ts us : List PTree) : (butcherProduct ts (node us)).treeFactorial = (orderList ts + (node us).order) * (treeFactorialList ts * treeFactorialList us)

theorem HopfAlgebras.PTree.forall2_perm_right {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {l2 l3 : List β} (hp : l2.Perm l3) {l1 : List α} : List.Forall₂ R l1 l2 → ∃ (l1' : List α), l1.Perm l1' ∧ List.Forall₂ R l1' l3

If a relation R holds elementwise between l1 and l2, then after permuting l2 we can permute l1 so that R still holds elementwise.

def HopfAlgebras.PTree.ListRelPerm {α : Type u_1} {β : Type u_2} (R : α → β → Prop) (xs : List α) (ys : List β) : Prop

Lists related elementwise up to a permutation of the left list.

Equations

• HopfAlgebras.PTree.ListRelPerm R xs ys = ∃ (xs' : List α), xs.Perm xs' ∧ List.Forall₂ R xs' ys

theorem HopfAlgebras.PTree.ListRelPerm.of_forall₂ {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {xs : List α} {ys : List β} (h : List.Forall₂ R xs ys) : ListRelPerm R xs ys

theorem HopfAlgebras.PTree.ListRelPerm.perm_left {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {xs xs' : List α} {ys : List β} (hp : xs.Perm xs') (h : ListRelPerm R xs' ys) : ListRelPerm R xs ys

theorem HopfAlgebras.PTree.ListRelPerm.of_perm_left_forall₂ {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {xs xs' : List α} {ys : List β} (hp : xs.Perm xs') (h : List.Forall₂ R xs' ys) : ListRelPerm R xs ys

theorem HopfAlgebras.PTree.ListRelPerm.map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {R : α → β → Prop} {S : γ → δ → Prop} {xs : List α} {ys : List β} {f : α → γ} {g : β → δ} (hS : ∀ {x : α} {y : β}, R x y → S (f x) (g y)) (h : ListRelPerm R xs ys) : ListRelPerm S (List.map f xs) (List.map g ys)

theorem HopfAlgebras.PTree.ListRelPerm.cons {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {x : α} {y : β} {xs : List α} {ys : List β} (hxy : R x y) (h : ListRelPerm R xs ys) : ListRelPerm R (x :: xs) (y :: ys)

theorem HopfAlgebras.PTree.ListRelPerm.refl {α : Type u_1} {R : α → α → Prop} (hrefl : ∀ (x : α), R x x) (xs : List α) : ListRelPerm R xs xs

theorem HopfAlgebras.PTree.ListRelPerm.append {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {xs₁ xs₂ : List α} {ys₁ ys₂ : List β} (h₁ : ListRelPerm R xs₁ ys₁) (h₂ : ListRelPerm R xs₂ ys₂) : ListRelPerm R (xs₁ ++ xs₂) (ys₁ ++ ys₂)

theorem HopfAlgebras.PTree.ListRelPerm.trans {α : Type u_1} {R : α → α → Prop} (htrans : ∀ {x y z : α}, R x y → R y z → R x z) {xs ys zs : List α} (hxy : ListRelPerm R xs ys) (hyz : ListRelPerm R ys zs) : ListRelPerm R xs zs

theorem HopfAlgebras.PTree.ListRelPerm.perm_of_eq {α : Type u_1} {xs ys : List α} (h : ListRelPerm (fun (x y : α) => x = y) xs ys) : xs.Perm ys

theorem HopfAlgebras.PTree.ListRelPerm.map_eq_perm {α : Type u_1} {β : Type u_2} {γ : Type u_3} {R : α → β → Prop} {xs : List α} {ys : List β} {f : α → γ} {g : β → γ} (hfg : ∀ {x : α} {y : β}, R x y → f x = g y) (h : ListRelPerm R xs ys) : (List.map f xs).Perm (List.map g ys)

theorem HopfAlgebras.PTree.ListRelPerm.flatMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {R : α → β → Prop} {S : γ → δ → Prop} {xs : List α} {ys : List β} {f : α → List γ} {g : β → List δ} (hfg : ∀ {x : α} {y : β}, R x y → ListRelPerm S (f x) (g y)) (h : ListRelPerm R xs ys) : ListRelPerm S (List.flatMap f xs) (List.flatMap g ys)

theorem HopfAlgebras.PTree.orderList_perm {ts1 ts2 : List PTree} (h : ts1.Perm ts2) : orderList ts1 = orderList ts2

orderList is invariant under permuting a list of planar trees.

theorem HopfAlgebras.PTree.treeFactorialList_perm {ts1 ts2 : List PTree} (h : ts1.Perm ts2) : treeFactorialList ts1 = treeFactorialList ts2

treeFactorialList is invariant under permuting a list of planar trees.

theorem HopfAlgebras.PTree.Perm.refl (t : PTree) : t.Perm t

PTree.Perm is reflexive.

theorem HopfAlgebras.PTree.permForall2_refl (ts : List PTree) : List.Forall₂ Perm ts ts

Elementwise reflexivity for PTree.Perm.

theorem HopfAlgebras.PTree.permForall2_symm {ts1 ts2 : List PTree} : List.Forall₂ Perm ts1 ts2 → List.Forall₂ Perm ts2 ts1

Elementwise symmetry for PTree.Perm.

theorem HopfAlgebras.PTree.Perm.symm {t1 t2 : PTree} : t1.Perm t2 → t2.Perm t1

PTree.Perm is symmetric.

theorem HopfAlgebras.PTree.permForall2_trans {ts1 ts2 ts3 : List PTree} : List.Forall₂ Perm ts1 ts2 → List.Forall₂ Perm ts2 ts3 → List.Forall₂ Perm ts1 ts3

Elementwise transitivity for PTree.Perm.

theorem HopfAlgebras.PTree.Perm.trans {t1 t2 t3 : PTree} : t1.Perm t2 → t2.Perm t3 → t1.Perm t3

PTree.Perm is transitive.

theorem HopfAlgebras.PTree.Perm.order_eq {t1 t2 : PTree} : t1.Perm t2 → t1.order = t2.order

PTree.Perm preserves the number of vertices.

theorem HopfAlgebras.PTree.orderList_eq_of_forall2 {ts1 ts2 : List PTree} : List.Forall₂ Perm ts1 ts2 → orderList ts1 = orderList ts2

Elementwise PTree.Perm preserves the total number of vertices.

theorem HopfAlgebras.PTree.Perm.treeFactorial_eq {t1 t2 : PTree} : t1.Perm t2 → t1.treeFactorial = t2.treeFactorial

PTree.Perm preserves Butcher's tree factorial.

theorem HopfAlgebras.PTree.treeFactorialList_eq_of_forall2 {ts1 ts2 : List PTree} : List.Forall₂ Perm ts1 ts2 → treeFactorialList ts1 = treeFactorialList ts2

Elementwise PTree.Perm preserves the product of tree factorials.

@[implicit_reducible]

instance HopfAlgebras.PTree.instSetoid : Setoid PTree

Equations

• HopfAlgebras.PTree.instSetoid = { r := HopfAlgebras.PTree.Perm, iseqv := HopfAlgebras.PTree.instSetoid._proof_1 }

theorem HopfAlgebras.PTree.perm_node_of_forall2 {ts1 ts2 : List PTree} (h : List.Forall₂ Perm ts1 ts2) : (node ts1).Perm (node ts2)

If the children are pairwise permutation-equivalent, then the nodes are too.

@[reducible, inline]

abbrev HopfAlgebras.RootedTree : Type

Non-empty non-planar rooted trees are planar rooted trees modulo PTree.Perm.

Equations

• HopfAlgebras.RootedTree = Quotient inferInstance

def HopfAlgebras.RootedTree.ofPTree (t : PTree) : RootedTree

The quotient map from planar rooted trees to non-planar rooted trees.

Equations

• HopfAlgebras.RootedTree.ofPTree t = ⟦t⟧

theorem HopfAlgebras.RootedTree.ofPTree_eq_iff {t u : PTree} : ofPTree t = ofPTree u ↔ t.Perm u

def HopfAlgebras.RootedTree.bullet : RootedTree

The one-vertex non-planar rooted tree.

Equations

• HopfAlgebras.RootedTree.bullet = HopfAlgebras.RootedTree.ofPTree HopfAlgebras.PTree.bullet

def HopfAlgebras.RootedTree.chain2 : RootedTree

The two-vertex non-planar rooted tree.

Equations

• HopfAlgebras.RootedTree.chain2 = HopfAlgebras.RootedTree.ofPTree HopfAlgebras.PTree.chain2

def HopfAlgebras.RootedTree.chain3 : RootedTree

The three-vertex non-planar chain.

Equations

• HopfAlgebras.RootedTree.chain3 = HopfAlgebras.RootedTree.ofPTree HopfAlgebras.PTree.chain3

def HopfAlgebras.RootedTree.cherry : RootedTree

A root with two bullet children.

Equations

• HopfAlgebras.RootedTree.cherry = HopfAlgebras.RootedTree.ofPTree HopfAlgebras.PTree.cherry

def HopfAlgebras.RootedTree.order : RootedTree → ℕ

The number of vertices of a non-planar rooted tree.

Equations

• HopfAlgebras.RootedTree.order = Quotient.lift HopfAlgebras.PTree.order ⋯

def HopfAlgebras.RootedTree.IsOfOrder (τ : RootedTree) (n : ℕ) : Prop

Predicate for non-empty rooted trees of a fixed order.

Equations

• τ.IsOfOrder n = (τ.order = n)

@[simp]

theorem HopfAlgebras.RootedTree.order_ofPTree (t : PTree) : (ofPTree t).order = t.order

@[simp]

theorem HopfAlgebras.RootedTree.order_bullet : bullet.order = 1

@[simp]

theorem HopfAlgebras.RootedTree.order_chain2 : chain2.order = 2

@[simp]

theorem HopfAlgebras.RootedTree.order_chain3 : chain3.order = 3

@[simp]

theorem HopfAlgebras.RootedTree.order_cherry : cherry.order = 3

theorem HopfAlgebras.RootedTree.order_pos (τ : RootedTree) : 0 < τ.order

theorem HopfAlgebras.RootedTree.order_eq_one_iff (τ : RootedTree) : τ.order = 1 ↔ τ = bullet

theorem HopfAlgebras.RootedTree.order_eq_two_iff (τ : RootedTree) : τ.order = 2 ↔ τ = chain2

theorem HopfAlgebras.RootedTree.order_eq_three_iff (τ : RootedTree) : τ.order = 3 ↔ τ = chain3 ∨ τ = cherry

def HopfAlgebras.RootedTree.treeFactorial : RootedTree → ℕ

Butcher's tree factorial for non-planar rooted trees.

Equations

• HopfAlgebras.RootedTree.treeFactorial = Quotient.lift HopfAlgebras.PTree.treeFactorial ⋯

@[simp]

theorem HopfAlgebras.RootedTree.treeFactorial_ofPTree (t : PTree) : (ofPTree t).treeFactorial = t.treeFactorial

@[simp]

theorem HopfAlgebras.RootedTree.ofPTree_out (τ : RootedTree) : ofPTree (Quotient.out τ) = τ

theorem HopfAlgebras.RootedTree.out_perm_ofPTree (t : PTree) : (Quotient.out (ofPTree t)).Perm t

theorem HopfAlgebras.RootedTree.map_ofPTree_eq_of_forall₂_perm {ts us : List PTree} : List.Forall₂ PTree.Perm ts us → List.map ofPTree ts = List.map ofPTree us

@[simp]

theorem HopfAlgebras.RootedTree.treeFactorial_bullet : bullet.treeFactorial = 1

@[simp]

theorem HopfAlgebras.RootedTree.treeFactorial_chain2 : chain2.treeFactorial = 2

@[simp]

theorem HopfAlgebras.RootedTree.treeFactorial_chain3 : chain3.treeFactorial = 6

@[simp]

theorem HopfAlgebras.RootedTree.treeFactorial_cherry : cherry.treeFactorial = 3

theorem HopfAlgebras.RootedTree.treeFactorial_pos (τ : RootedTree) : 0 < τ.treeFactorial

theorem HopfAlgebras.RootedTree.treeFactorial_ne_zero (τ : RootedTree) : τ.treeFactorial ≠ 0

inductive HopfAlgebras.TreeIndex : Type

Rooted trees with an adjoined empty tree, as used for B-series coefficients.

• empty : TreeIndex
• tree : RootedTree → TreeIndex

def HopfAlgebras.TreeIndex.bullet : TreeIndex

The one-vertex tree as a B-series index.

Equations

• HopfAlgebras.TreeIndex.bullet = HopfAlgebras.TreeIndex.tree HopfAlgebras.RootedTree.bullet

def HopfAlgebras.TreeIndex.chain2 : TreeIndex

The two-vertex tree as a B-series index.

Equations

• HopfAlgebras.TreeIndex.chain2 = HopfAlgebras.TreeIndex.tree HopfAlgebras.RootedTree.chain2

def HopfAlgebras.TreeIndex.chain3 : TreeIndex

The three-vertex chain as a B-series index.

Equations

• HopfAlgebras.TreeIndex.chain3 = HopfAlgebras.TreeIndex.tree HopfAlgebras.RootedTree.chain3

def HopfAlgebras.TreeIndex.cherry : TreeIndex

The cherry tree as a B-series index.

Equations

• HopfAlgebras.TreeIndex.cherry = HopfAlgebras.TreeIndex.tree HopfAlgebras.RootedTree.cherry

def HopfAlgebras.TreeIndex.order : TreeIndex → ℕ

The order of a B-series tree index.

Equations

• HopfAlgebras.TreeIndex.empty.order = 0
• (HopfAlgebras.TreeIndex.tree τ).order = τ.order

def HopfAlgebras.TreeIndex.IsOfOrder (τ : TreeIndex) (n : ℕ) : Prop

Predicate for B-series tree indices of a fixed order.

Equations

• τ.IsOfOrder n = (τ.order = n)

def HopfAlgebras.TreeIndex.treeFactorial : TreeIndex → ℕ

Butcher's tree factorial for B-series tree indices.

Equations

• HopfAlgebras.TreeIndex.empty.treeFactorial = 1
• (HopfAlgebras.TreeIndex.tree τ).treeFactorial = τ.treeFactorial

@[simp]

theorem HopfAlgebras.TreeIndex.order_empty : empty.order = 0

@[simp]

theorem HopfAlgebras.TreeIndex.order_tree (τ : RootedTree) : (tree τ).order = τ.order

@[simp]

theorem HopfAlgebras.TreeIndex.order_bullet : bullet.order = 1

@[simp]

theorem HopfAlgebras.TreeIndex.order_chain2 : chain2.order = 2

@[simp]

theorem HopfAlgebras.TreeIndex.order_chain3 : chain3.order = 3

@[simp]

theorem HopfAlgebras.TreeIndex.order_cherry : cherry.order = 3

@[simp]

theorem HopfAlgebras.TreeIndex.order_eq_zero_iff (τ : TreeIndex) : τ.order = 0 ↔ τ = empty

theorem HopfAlgebras.TreeIndex.order_pos_iff_ne_empty (τ : TreeIndex) : 0 < τ.order ↔ τ ≠ empty

@[simp]

theorem HopfAlgebras.TreeIndex.order_eq_one_iff (τ : TreeIndex) : τ.order = 1 ↔ τ = bullet

theorem HopfAlgebras.TreeIndex.order_eq_two_iff (τ : TreeIndex) : τ.order = 2 ↔ τ = chain2

theorem HopfAlgebras.TreeIndex.order_eq_three_iff (τ : TreeIndex) : τ.order = 3 ↔ τ = chain3 ∨ τ = cherry

@[simp]

theorem HopfAlgebras.TreeIndex.treeFactorial_empty : empty.treeFactorial = 1

@[simp]

theorem HopfAlgebras.TreeIndex.treeFactorial_tree (τ : RootedTree) : (tree τ).treeFactorial = τ.treeFactorial

@[simp]

theorem HopfAlgebras.TreeIndex.treeFactorial_bullet : bullet.treeFactorial = 1

@[simp]

theorem HopfAlgebras.TreeIndex.treeFactorial_chain2 : chain2.treeFactorial = 2

@[simp]

theorem HopfAlgebras.TreeIndex.treeFactorial_chain3 : chain3.treeFactorial = 6

@[simp]

theorem HopfAlgebras.TreeIndex.treeFactorial_cherry : cherry.treeFactorial = 3

theorem HopfAlgebras.TreeIndex.treeFactorial_pos (τ : TreeIndex) : 0 < τ.treeFactorial

theorem HopfAlgebras.TreeIndex.treeFactorial_ne_zero (τ : TreeIndex) : τ.treeFactorial ≠ 0