Registry · Definition II.D01 established formalized

II.D01 — Split-Complex Codomain H_tau

Split-Complex Codomain H_tau

Book II Part 0 Ch. 2

Dependency Graph

Depends on (2)

I.D20 I.D19

Lean Formalization

Module: TauLib.BookII.Prologue.SplitComplexInterior

Symbol: Tau.BookII.Prologue.HTau