Registry · Definition I.D85 established formalized

I.D85 — Elliptic Complex Field

TauComplex = TauReal[i]/(i^2+1): the elliptic complex field. Pairs (re, im) of TauReal values with multiplication (ac-bd, ad+bc). The imaginary unit i satisfies i^2 = -1.

Book I Part 17 Ch. 77

Dependency Graph

Depends on (2)

Depended on by (3)

Lean Formalization

Module: TauLib.BookI.Boundary.ComplexField

Symbol: Tau.Boundary.TauComplex