Registry · Theorem I.T43 established formalized

I.T43 — TauComplex Ring Axioms

TauComplex satisfies all commutative ring axioms including i^2=-1. Each axiom reduces through TauReal to TauRat algebra via the toInt bridge.

Book I Part 17 Ch. 77

Dependency Graph

Depends on (2)

I.D85 I.P39

Lean Formalization

Module: TauLib.BookI.Boundary.ComplexField

Symbol: Tau.Boundary.taucomplex_ring_axioms