Registry · Lemma II.L12 established formalized

II.L12 — Extension in Split-Complex Codomain

Extension in Split-Complex Codomain

Book II Part 9 Ch. 48

Dependency Graph

Depends on (7)

II.D36 II.D59 II.P13 II.T26 II.D35 I.D21 I.T31

Depended on by (2)

II.T37 II.T40

Lean Formalization

Module: TauLib.BookII.CentralTheorem.HartogsExtension

Symbol: Tau.BookII.CentralTheorem.extension_channel_check