Registry · Definition II.D45 established formalized

II.D45 — Canonical Holomorphic Basis

Canonical Holomorphic Basis

Book II Part 6 Ch. 35

Dependency Graph

Depends on (3)

II.D46 I.T18 I.D21

Depended on by (7)

II.D47 II.D51 II.D52 II.D82 II.L07 II.L09 II.T31

Lean Formalization

Module: TauLib.BookII.Hartogs.CanonicalBasis

Symbol: canonical_basis_check