Registry · Proposition II.P09 established formalized

II.P09 — Decomposition Functoriality

Decomposition Functoriality

Book II Part 7 Ch. 37

Dependency Graph

Depends on (4)

I.D21 I.T10 II.D48 II.L07

Lean Formalization

Module: TauLib.BookII.Regularity.IdempotentDecomposition

Symbol: decompose_functoriality_check