Registry · Proposition II.P11 established formalized

II.P11 — Hom Bipolar Decomposition

Hom Bipolar Decomposition

Book II Part 8 Ch. 42

Dependency Graph

Depends on (4)

I.D21 I.T05 II.L07 II.D54

Depended on by (3)

II.D55 II.D56 II.T36

Lean Formalization

Module: TauLib.BookII.Enrichment.SelfEnrichment

Symbol: Tau.BookII.Enrichment.hom_bipolar_check