Registry · Definition II.D39 established formalized

II.D39 — Composition of Holomorphic Maps

Composition of Holomorphic Maps

Book II Part 6 Ch. 33

Dependency Graph

Depends on (4)

I.D49 I.D20 I.T18 II.T26

Depended on by (3)

II.D40 II.D41 II.T29

Lean Formalization

Module: TauLib.BookII.Hartogs.CategoryStructure

Symbol: hol_compose