Registry · Lemma II.L08 established formalized

II.L08 — Branch Factorization

Branch Factorization

Book II Part 7 Ch. 38

Dependency Graph

Depends on (5)

II.L07 II.D48 II.D37 I.D21 I.T10

Depended on by (3)

II.L09 II.L10 II.T33

Lean Formalization

Module: TauLib.BookII.Regularity.ThreeLemmaChain

Symbol: branch_factorization_check