Labelled Rooted Trees

This file defines rooted trees whose vertices carry labels. As with HopfAlgebras.Trees.Rooted, the planar type is primary and the non-planar type is the quotient by recursively permuting children.

Main definitions

• PLTree α - non-empty planar rooted trees labelled by α
• PLTree.Perm - equivalence relation forgetting planar child order
• LRootedTree α - non-empty non-planar labelled rooted trees
• LRootedTree.rootLabel - the label at the root
• PLTree.erase and LRootedTree.erase - forget labels
• PLTree.treeFactorial and LRootedTree.treeFactorial - Butcher tree factorials

inductive HopfAlgebras.PLTree (α : Type u) : Type u

Non-empty planar rooted trees with one label at each vertex.

• node {α : Type u} : α → List (PLTree α) → PLTree α

partial def HopfAlgebras.instReprPLTree.repr {α✝ : Type u_1} [Repr α✝] : PLTree α✝ → ℕ → Std.Format

@[implicit_reducible]

instance HopfAlgebras.instReprPLTree {α✝ : Type u_1} [Repr α✝] : Repr (PLTree α✝)

Equations

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

@[irreducible]

def HopfAlgebras.PLTree.erase {α : Type u} : PLTree α → PTree

Forget labels from a planar labelled rooted tree.

Equations

• (HopfAlgebras.PLTree.node a a_1).erase = HopfAlgebras.PTree.node (List.map HopfAlgebras.PLTree.erase a_1)

@[irreducible]

def HopfAlgebras.PLTree.constLabel {α : Type u} (a : α) : PTree → PLTree α

Label every vertex of a planar rooted tree by the same label.

Equations

• HopfAlgebras.PLTree.constLabel a (HopfAlgebras.PTree.node ts) = HopfAlgebras.PLTree.node a (List.map (HopfAlgebras.PLTree.constLabel a) ts)

def HopfAlgebras.PLTree.rootLabel {α : Type u} : PLTree α → α

The label at the root of a planar labelled rooted tree.

Equations

• (HopfAlgebras.PLTree.node a a_1).rootLabel = a

def HopfAlgebras.PLTree.order {α : Type u} : PLTree α → ℕ

The number of vertices of a planar labelled rooted tree.

Equations

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

def HopfAlgebras.PLTree.orderList {α : Type u} : List (PLTree α) → ℕ

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

Equations

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

@[irreducible]

def HopfAlgebras.PLTree.map {α : Type u} {β : Type v} (f : α → β) : PLTree α → PLTree β

Change all labels in a planar labelled rooted tree.

Equations

• HopfAlgebras.PLTree.map f (HopfAlgebras.PLTree.node a a_1) = HopfAlgebras.PLTree.node (f a) (List.map (HopfAlgebras.PLTree.map f) a_1)

def HopfAlgebras.PLTree.treeFactorial {α : Type u} (t : PLTree α) : ℕ

Butcher's tree factorial, ignoring labels.

Equations

• t.treeFactorial = t.erase.treeFactorial

def HopfAlgebras.PLTree.treeFactorialList {α : Type u} (ts : List (PLTree α)) : ℕ

Product of tree factorials over a list of labelled planar rooted trees.

Equations

• HopfAlgebras.PLTree.treeFactorialList ts = (List.map HopfAlgebras.PLTree.treeFactorial ts).prod

inductive HopfAlgebras.PLTree.Perm {α : Type u} : PLTree α → PLTree α → Prop

Two labelled planar trees are equivalent if labels agree and children are permuted recursively.

• node {α : Type u} {a : α} {ts us ts' : List (PLTree α)} : ts.Perm ts' → List.Forall₂ Perm ts' us → (PLTree.node a ts).Perm (PLTree.node a us)

@[simp]

theorem HopfAlgebras.PLTree.erase_node {α : Type u} (a : α) (ts : List (PLTree α)) : (node a ts).erase = PTree.node (List.map erase ts)

@[simp]

theorem HopfAlgebras.PLTree.constLabel_node {α : Type u} (a : α) (ts : List PTree) : constLabel a (PTree.node ts) = node a (List.map (constLabel a) ts)

@[simp]

theorem HopfAlgebras.PLTree.erase_constLabel {α : Type u} (a : α) (t : PTree) : (constLabel a t).erase = t

@[simp]

theorem HopfAlgebras.PLTree.eraseList_constLabel {α : Type u} (a : α) (ts : List PTree) : List.map erase (List.map (constLabel a) ts) = ts

@[simp]

theorem HopfAlgebras.PLTree.rootLabel_node {α : Type u} (a : α) (ts : List (PLTree α)) : (node a ts).rootLabel = a

@[simp]

theorem HopfAlgebras.PLTree.rootLabel_constLabel {α : Type u} (a : α) (t : PTree) : (constLabel a t).rootLabel = a

@[simp]

theorem HopfAlgebras.PLTree.order_node {α : Type u} (a : α) (ts : List (PLTree α)) : (node a ts).order = 1 + orderList ts

@[simp]

theorem HopfAlgebras.PLTree.orderList_nil {α : Type u} : orderList [] = 0

@[simp]

theorem HopfAlgebras.PLTree.orderList_cons {α : Type u} (t : PLTree α) (ts : List (PLTree α)) : orderList (t :: ts) = t.order + orderList ts

@[simp]

theorem HopfAlgebras.PLTree.map_node {α : Type u} {β : Type v} (f : α → β) (a : α) (ts : List (PLTree α)) : map f (node a ts) = node (f a) (List.map (map f) ts)

@[simp]

theorem HopfAlgebras.PLTree.rootLabel_map {α : Type u} {β : Type v} (f : α → β) (t : PLTree α) : (map f t).rootLabel = f t.rootLabel

@[simp]

theorem HopfAlgebras.PLTree.map_constLabel {α : Type u} {β : Type v} (f : α → β) (a : α) (t : PTree) : map f (constLabel a t) = constLabel (f a) t

@[simp]

theorem HopfAlgebras.PLTree.mapList_constLabel {α : Type u} {β : Type v} (f : α → β) (a : α) (ts : List PTree) : List.map (map f) (List.map (constLabel a) ts) = List.map (constLabel (f a)) ts

@[simp]

theorem HopfAlgebras.PLTree.treeFactorialList_nil {α : Type u} : treeFactorialList [] = 1

@[simp]

theorem HopfAlgebras.PLTree.treeFactorialList_cons {α : Type u} (t : PLTree α) (ts : List (PLTree α)) : treeFactorialList (t :: ts) = t.treeFactorial * treeFactorialList ts

theorem HopfAlgebras.PLTree.treeFactorialList_erase {α : Type u} (ts : List (PLTree α)) : PTree.treeFactorialList (List.map erase ts) = treeFactorialList ts

theorem HopfAlgebras.PLTree.treeFactorial_pos {α : Type u} (t : PLTree α) : 0 < t.treeFactorial

theorem HopfAlgebras.PLTree.treeFactorial_ne_zero {α : Type u} (t : PLTree α) : t.treeFactorial ≠ 0

theorem HopfAlgebras.PLTree.treeFactorialList_pos {α : Type u} (ts : List (PLTree α)) : 0 < treeFactorialList ts

theorem HopfAlgebras.PLTree.treeFactorialList_ne_zero {α : Type u} (ts : List (PLTree α)) : treeFactorialList ts ≠ 0

@[simp]

theorem HopfAlgebras.PLTree.treeFactorialList_append {α : Type u} (ts us : List (PLTree α)) : treeFactorialList (ts ++ us) = treeFactorialList ts * treeFactorialList us

@[simp]

theorem HopfAlgebras.PLTree.orderList_append {α : Type u} (ts us : List (PLTree α)) : orderList (ts ++ us) = orderList ts + orderList us

theorem HopfAlgebras.PLTree.order_pos {α : Type u} (t : PLTree α) : 0 < t.order

@[simp]

theorem HopfAlgebras.PLTree.order_erase {α : Type u} (t : PLTree α) : t.erase.order = t.order

@[simp]

theorem HopfAlgebras.PLTree.orderList_erase {α : Type u} (ts : List (PLTree α)) : PTree.orderList (List.map erase ts) = orderList ts

@[simp]

theorem HopfAlgebras.PLTree.treeFactorial_node {α : Type u} (a : α) (ts : List (PLTree α)) : (node a ts).treeFactorial = (node a ts).order * treeFactorialList ts

@[simp]

theorem HopfAlgebras.PLTree.order_map {α : Type u} {β : Type v} (f : α → β) (t : PLTree α) : (map f t).order = t.order

@[simp]

theorem HopfAlgebras.PLTree.orderList_map {α : Type u} {β : Type v} (f : α → β) (ts : List (PLTree α)) : orderList (List.map (map f) ts) = orderList ts

@[simp]

theorem HopfAlgebras.PLTree.erase_map {α : Type u} {β : Type v} (f : α → β) (t : PLTree α) : (map f t).erase = t.erase

@[simp]

theorem HopfAlgebras.PLTree.eraseList_map {α : Type u} {β : Type v} (f : α → β) (ts : List (PLTree α)) : List.map erase (List.map (map f) ts) = List.map erase ts

def HopfAlgebras.PLTree.butcherProduct {α : Type u} (ts : List (PLTree α)) : PLTree α → PLTree α

Attach an ordered labelled forest as the first children of the root.

Equations

• HopfAlgebras.PLTree.butcherProduct ts (HopfAlgebras.PLTree.node a a_1) = HopfAlgebras.PLTree.node a (ts ++ a_1)

@[simp]

theorem HopfAlgebras.PLTree.butcherProduct_node {α : Type u} (ts us : List (PLTree α)) (a : α) : butcherProduct ts (node a us) = node a (ts ++ us)

@[simp]

theorem HopfAlgebras.PLTree.rootLabel_butcherProduct {α : Type u} (ts : List (PLTree α)) (t : PLTree α) : (butcherProduct ts t).rootLabel = t.rootLabel

@[simp]

theorem HopfAlgebras.PLTree.butcherProduct_nil {α : Type u} (t : PLTree α) : butcherProduct [] t = t

@[simp]

theorem HopfAlgebras.PLTree.butcherProduct_assoc {α : Type u} (ts us : List (PLTree α)) (t : PLTree α) : butcherProduct ts (butcherProduct us t) = butcherProduct (ts ++ us) t

@[simp]

theorem HopfAlgebras.PLTree.order_butcherProduct {α : Type u} (ts : List (PLTree α)) (t : PLTree α) : (butcherProduct ts t).order = orderList ts + t.order

@[simp]

theorem HopfAlgebras.PLTree.erase_butcherProduct {α : Type u} (ts : List (PLTree α)) (t : PLTree α) : (butcherProduct ts t).erase = PTree.butcherProduct (List.map erase ts) t.erase

@[simp]

theorem HopfAlgebras.PLTree.map_butcherProduct {α : Type u} {β : Type v} (f : α → β) (ts : List (PLTree α)) (t : PLTree α) : map f (butcherProduct ts t) = butcherProduct (List.map (map f) ts) (map f t)

@[simp]

theorem HopfAlgebras.PLTree.butcherProduct_constLabel {α : Type u} (a : α) (ts : List PTree) (t : PTree) : butcherProduct (List.map (constLabel a) ts) (constLabel a t) = constLabel a (PTree.butcherProduct ts t)

theorem HopfAlgebras.PLTree.treeFactorial_butcherProduct {α : Type u} (ts us : List (PLTree α)) (a : α) : (butcherProduct ts (node a us)).treeFactorial = (orderList ts + (node a us).order) * (treeFactorialList ts * treeFactorialList us)

@[simp]

theorem HopfAlgebras.PLTree.map_id {α : Type u} (t : PLTree α) : map id t = t

@[simp]

theorem HopfAlgebras.PLTree.mapList_id {α : Type u} (ts : List (PLTree α)) : List.map (map id) ts = ts

@[simp]

theorem HopfAlgebras.PLTree.map_comp {α : Type u} {β : Type v} {γ : Type w} (g : β → γ) (f : α → β) (t : PLTree α) : map g (map f t) = map (g ∘ f) t

@[simp]

theorem HopfAlgebras.PLTree.mapList_comp {α : Type u} {β : Type v} {γ : Type w} (g : β → γ) (f : α → β) (ts : List (PLTree α)) : List.map (map g) (List.map (map f) ts) = List.map (map (g ∘ f)) ts

theorem HopfAlgebras.PLTree.map_injective {α : Type u} {β : Type v} (f : α → β) (hf : Function.Injective f) : Function.Injective (map f)

theorem HopfAlgebras.PLTree.map_eq_map_iff_of_injective {α : Type u} {β : Type v} (f : α → β) (hf : Function.Injective f) {t u : PLTree α} : map f t = map f u ↔ t = u

@[simp]

theorem HopfAlgebras.PLTree.treeFactorial_map {α : Type u} {β : Type v} (f : α → β) (t : PLTree α) : (map f t).treeFactorial = t.treeFactorial

theorem HopfAlgebras.PLTree.erase_order_eq_order {α : Type u} (t : PLTree α) : t.erase.order = t.order

theorem HopfAlgebras.PLTree.orderList_perm {α : Type u} {ts us : List (PLTree α)} (h : ts.Perm us) : orderList ts = orderList us

theorem HopfAlgebras.PLTree.eraseList_perm {α : Type u} {ts us : List (PLTree α)} (h : ts.Perm us) : (List.map erase ts).Perm (List.map erase us)

theorem HopfAlgebras.PLTree.Perm.refl {α : Type u} (t : PLTree α) : t.Perm t

PLTree.Perm is reflexive.

theorem HopfAlgebras.PLTree.permForall₂_refl {α : Type u} (ts : List (PLTree α)) : List.Forall₂ Perm ts ts

Elementwise reflexivity for PLTree.Perm.

theorem HopfAlgebras.PLTree.permForall₂_symm {α : Type u} {ts us : List (PLTree α)} : List.Forall₂ Perm ts us → List.Forall₂ Perm us ts

Elementwise symmetry for PLTree.Perm.

theorem HopfAlgebras.PLTree.Perm.symm {α : Type u} {t u : PLTree α} : t.Perm u → u.Perm t

PLTree.Perm is symmetric.

theorem HopfAlgebras.PLTree.permForall₂_trans {α : Type u} {ts us vs : List (PLTree α)} : List.Forall₂ Perm ts us → List.Forall₂ Perm us vs → List.Forall₂ Perm ts vs

Elementwise transitivity for PLTree.Perm.

theorem HopfAlgebras.PLTree.Perm.trans {α : Type u} {t u v : PLTree α} : t.Perm u → u.Perm v → t.Perm v

PLTree.Perm is transitive.

theorem HopfAlgebras.PLTree.Perm.order_eq {α : Type u} {t u : PLTree α} : t.Perm u → t.order = u.order

theorem HopfAlgebras.PLTree.orderList_eq_of_forall₂ {α : Type u} {ts us : List (PLTree α)} : List.Forall₂ Perm ts us → orderList ts = orderList us

theorem HopfAlgebras.PLTree.Perm.rootLabel_eq {α : Type u} {t u : PLTree α} : t.Perm u → t.rootLabel = u.rootLabel

theorem HopfAlgebras.PLTree.Perm.erase_perm {α : Type u} {t u : PLTree α} : t.Perm u → t.erase.Perm u.erase

theorem HopfAlgebras.PLTree.erase_forall₂_perm {α : Type u} {ts us : List (PLTree α)} : List.Forall₂ Perm ts us → List.Forall₂ PTree.Perm (List.map erase ts) (List.map erase us)

theorem HopfAlgebras.PLTree.Perm.treeFactorial_eq {α : Type u} {t u : PLTree α} (h : t.Perm u) : t.treeFactorial = u.treeFactorial

theorem HopfAlgebras.PLTree.Perm.map {α : Type u} {β : Type v} (f : α → β) {t u : PLTree α} : t.Perm u → (PLTree.map f t).Perm (PLTree.map f u)

theorem HopfAlgebras.PLTree.map_forall₂ {α : Type u} {β : Type v} (f : α → β) {ts us : List (PLTree α)} : List.Forall₂ Perm ts us → List.Forall₂ Perm (List.map (map f) ts) (List.map (map f) us)

theorem HopfAlgebras.PLTree.constLabel_perm {α : Type u} (a : α) {t u : PTree} : t.Perm u → (constLabel a t).Perm (constLabel a u)

theorem HopfAlgebras.PLTree.constLabel_forall₂ {α : Type u} (a : α) {ts us : List PTree} : List.Forall₂ PTree.Perm ts us → List.Forall₂ Perm (List.map (constLabel a) ts) (List.map (constLabel a) us)

@[implicit_reducible]

instance HopfAlgebras.PLTree.instSetoid {α : Type u} : Setoid (PLTree α)

Equations

• HopfAlgebras.PLTree.instSetoid = { r := HopfAlgebras.PLTree.Perm, iseqv := ⋯ }

@[reducible, inline]

abbrev HopfAlgebras.LRootedTree (α : Type u) : Type u

Non-empty non-planar labelled rooted trees.

Equations

• HopfAlgebras.LRootedTree α = Quotient inferInstance

def HopfAlgebras.LRootedTree.ofPLTree {α : Type u} (t : PLTree α) : LRootedTree α

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

Equations

• HopfAlgebras.LRootedTree.ofPLTree t = ⟦t⟧

theorem HopfAlgebras.LRootedTree.ofPLTree_eq_iff {α : Type u} {t u : PLTree α} : ofPLTree t = ofPLTree u ↔ t.Perm u

def HopfAlgebras.LRootedTree.order {α : Type u} : LRootedTree α → ℕ

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

Equations

• HopfAlgebras.LRootedTree.order = Quotient.lift HopfAlgebras.PLTree.order ⋯

def HopfAlgebras.LRootedTree.rootLabel {α : Type u} : LRootedTree α → α

The label at the root of a non-planar labelled rooted tree.

Equations

• HopfAlgebras.LRootedTree.rootLabel = Quotient.lift HopfAlgebras.PLTree.rootLabel ⋯

def HopfAlgebras.LRootedTree.erase {α : Type u} : LRootedTree α → RootedTree

Forget labels from a non-planar labelled rooted tree.

Equations

• HopfAlgebras.LRootedTree.erase = Quotient.lift (fun (t : HopfAlgebras.PLTree α) => HopfAlgebras.RootedTree.ofPTree t.erase) ⋯

def HopfAlgebras.LRootedTree.constLabel {α : Type u} (a : α) : RootedTree → LRootedTree α

Label every vertex of a rooted tree by the same label.

Equations

• HopfAlgebras.LRootedTree.constLabel a = Quotient.lift (fun (t : HopfAlgebras.PTree) => HopfAlgebras.LRootedTree.ofPLTree (HopfAlgebras.PLTree.constLabel a t)) ⋯

def HopfAlgebras.LRootedTree.map {α : Type u} {β : Type v} (f : α → β) : LRootedTree α → LRootedTree β

Change all labels in a non-planar labelled rooted tree.

Equations

• HopfAlgebras.LRootedTree.map f = Quotient.lift (fun (t : HopfAlgebras.PLTree α) => HopfAlgebras.LRootedTree.ofPLTree (HopfAlgebras.PLTree.map f t)) ⋯

def HopfAlgebras.LRootedTree.treeFactorial {α : Type u} : LRootedTree α → ℕ

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

Equations

• HopfAlgebras.LRootedTree.treeFactorial = Quotient.lift HopfAlgebras.PLTree.treeFactorial ⋯

@[simp]

theorem HopfAlgebras.LRootedTree.order_ofPLTree {α : Type u} (t : PLTree α) : (ofPLTree t).order = t.order

@[simp]

theorem HopfAlgebras.LRootedTree.rootLabel_ofPLTree {α : Type u} (t : PLTree α) : (ofPLTree t).rootLabel = t.rootLabel

@[simp]

theorem HopfAlgebras.LRootedTree.erase_ofPLTree {α : Type u} (t : PLTree α) : (ofPLTree t).erase = RootedTree.ofPTree t.erase

theorem HopfAlgebras.LRootedTree.erase_out_perm {α : Type u} (τ : LRootedTree α) : (Quotient.out τ).erase.Perm (Quotient.out τ.erase)

@[simp]

theorem HopfAlgebras.LRootedTree.constLabel_ofPTree {α : Type u} (a : α) (t : PTree) : constLabel a (RootedTree.ofPTree t) = ofPLTree (PLTree.constLabel a t)

@[simp]

theorem HopfAlgebras.LRootedTree.rootLabel_constLabel {α : Type u} (a : α) (t : RootedTree) : (constLabel a t).rootLabel = a

@[simp]

theorem HopfAlgebras.LRootedTree.map_ofPLTree {α : Type u} {β : Type v} (f : α → β) (t : PLTree α) : map f (ofPLTree t) = ofPLTree (PLTree.map f t)

@[simp]

theorem HopfAlgebras.LRootedTree.treeFactorial_ofPLTree {α : Type u} (t : PLTree α) : (ofPLTree t).treeFactorial = t.treeFactorial

@[simp]

theorem HopfAlgebras.LRootedTree.ofPLTree_out {α : Type u} (τ : LRootedTree α) : ofPLTree (Quotient.out τ) = τ

theorem HopfAlgebras.LRootedTree.out_perm_ofPLTree {α : Type u} (t : PLTree α) : (Quotient.out (ofPLTree t)).Perm t

theorem HopfAlgebras.LRootedTree.map_out_perm {α : Type u} {β : Type v} (f : α → β) (τ : LRootedTree α) : (PLTree.map f (Quotient.out τ)).Perm (Quotient.out (map f τ))

theorem HopfAlgebras.LRootedTree.constLabel_out_perm {α : Type u} (a : α) (τ : RootedTree) : (PLTree.constLabel a (Quotient.out τ)).Perm (Quotient.out (constLabel a τ))

theorem HopfAlgebras.LRootedTree.map_ofPLTree_eq_of_forall₂_perm {α : Type u} {ts us : List (PLTree α)} : List.Forall₂ PLTree.Perm ts us → List.map ofPLTree ts = List.map ofPLTree us

@[simp]

theorem HopfAlgebras.LRootedTree.rootLabel_map {α : Type u} {β : Type v} (f : α → β) (t : LRootedTree α) : (map f t).rootLabel = f t.rootLabel

@[simp]

theorem HopfAlgebras.LRootedTree.map_constLabel {α : Type u} {β : Type v} (f : α → β) (a : α) (t : RootedTree) : map f (constLabel a t) = constLabel (f a) t

@[simp]

theorem HopfAlgebras.LRootedTree.erase_constLabel {α : Type u} (a : α) (t : RootedTree) : (constLabel a t).erase = t

theorem HopfAlgebras.LRootedTree.constLabel_injective {α : Type u} (a : α) : Function.Injective (constLabel a)

@[simp]

theorem HopfAlgebras.LRootedTree.constLabel_eq_constLabel_iff {α : Type u} (a : α) {s t : RootedTree} : constLabel a s = constLabel a t ↔ s = t

@[simp]

theorem HopfAlgebras.LRootedTree.order_erase {α : Type u} (t : LRootedTree α) : t.erase.order = t.order

@[simp]

theorem HopfAlgebras.LRootedTree.order_map {α : Type u} {β : Type v} (f : α → β) (t : LRootedTree α) : (map f t).order = t.order

@[simp]

theorem HopfAlgebras.LRootedTree.erase_map {α : Type u} {β : Type v} (f : α → β) (t : LRootedTree α) : (map f t).erase = t.erase

@[simp]

theorem HopfAlgebras.LRootedTree.treeFactorial_erase {α : Type u} (t : LRootedTree α) : t.erase.treeFactorial = t.treeFactorial

@[simp]

theorem HopfAlgebras.LRootedTree.order_constLabel {α : Type u} (a : α) (t : RootedTree) : (constLabel a t).order = t.order

@[simp]

theorem HopfAlgebras.LRootedTree.treeFactorial_constLabel {α : Type u} (a : α) (t : RootedTree) : (constLabel a t).treeFactorial = t.treeFactorial

@[simp]

theorem HopfAlgebras.LRootedTree.treeFactorial_map {α : Type u} {β : Type v} (f : α → β) (t : LRootedTree α) : (map f t).treeFactorial = t.treeFactorial

theorem HopfAlgebras.LRootedTree.treeFactorial_pos {α : Type u} (t : LRootedTree α) : 0 < t.treeFactorial

theorem HopfAlgebras.LRootedTree.treeFactorial_ne_zero {α : Type u} (t : LRootedTree α) : t.treeFactorial ≠ 0

@[simp]

theorem HopfAlgebras.LRootedTree.map_id {α : Type u} (t : LRootedTree α) : map id t = t

@[simp]

theorem HopfAlgebras.LRootedTree.map_comp {α : Type u} {β : Type v} {γ : Type w} (g : β → γ) (f : α → β) (t : LRootedTree α) : map g (map f t) = map (g ∘ f) t

theorem HopfAlgebras.LRootedTree.map_injective {α : Type u} {β : Type v} (f : α → β) (hf : Function.Injective f) : Function.Injective (map f)

theorem HopfAlgebras.LRootedTree.map_eq_map_iff_of_injective {α : Type u} {β : Type v} (f : α → β) (hf : Function.Injective f) {s t : LRootedTree α} : map f s = map f t ↔ s = t

theorem HopfAlgebras.LRootedTree.order_pos {α : Type u} (t : LRootedTree α) : 0 < t.order