Registry · Definition II.D48 established formalized

II.D48 — Canonical Decomposition

Canonical Decomposition

Book II Part 7 Ch. 37

Dependency Graph

Depends on (4)

I.D21 I.T10 II.D35 II.T27

Depended on by (3)

II.L08 II.P09 II.P13

Lean Formalization

Module: TauLib.BookII.Regularity.IdempotentDecomposition

Symbol: canonical_decomposition_check