No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
9structure TransferKernel (ι : Type) where
10 T : (ι → ℂ) →L[ℂ] (ι → ℂ)
11
used by (4)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (4)
Lean names referenced from this declaration's body.
-
T
in IndisputableMonolith.Foundation.Breath1024
decl_use
-
T
in IndisputableMonolith.Gap45.SyncMinimization
decl_use
-
L
in IndisputableMonolith.Recognition
decl_use
-
L
in IndisputableMonolith.Recognition.Cycle3
decl_use