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)
27noncomputable def buildKernelFromMatrix (ι : Type) [Fintype ι] [DecidableEq ι]
28 (V : MatrixView ι) : Σ K : TransferKernel ι, MatrixBridge ι K V :=
proof body
Definition body.
29by
30 let K : TransferKernel ι := { T := CLM.ofLM (Matrix.toLin' V.A) }
31 exact ⟨K, { intertwine := rfl }⟩
32
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (15)
Lean names referenced from this declaration's body.
-
K
in IndisputableMonolith.Constants
decl_use
-
K
in IndisputableMonolith.Constants.LambdaRecDerivation
decl_use
-
V
in IndisputableMonolith.Cosmology.InflatonPotentialFromJCost
decl_use
-
T
in IndisputableMonolith.Foundation.Breath1024
decl_use
-
A
in IndisputableMonolith.Foundation.IntegrationGap
decl_use
-
V
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
T
in IndisputableMonolith.Gap45.SyncMinimization
decl_use
-
A
in IndisputableMonolith.Masses.Anchor
decl_use
-
A
in IndisputableMonolith.Modal.Actualization
decl_use
-
MatrixBridge
in IndisputableMonolith.Relativity.Geometry.MatrixBridge
decl_use
-
V
in IndisputableMonolith.RRF.Core.Glossary
decl_use
-
CLM
in IndisputableMonolith.YM.Kernel
decl_use
-
MatrixBridge
in IndisputableMonolith.YM.Kernel
decl_use
-
MatrixView
in IndisputableMonolith.YM.Kernel
decl_use
-
TransferKernel
in IndisputableMonolith.YM.Kernel
decl_use