def definition def or abbrev

`KernelHasMatrixView`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  23def KernelHasMatrixView (ι : Type) [Fintype ι] [DecidableEq ι]
  24  (K : TransferKernel ι) (V : MatrixView ι) : Prop :=

Definition body.

  25  Nonempty (MatrixBridge ι K V)
  26

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
V in IndisputableMonolith.Foundation.SpectralEmergence decl_use
MatrixBridge in IndisputableMonolith.Relativity.Geometry.MatrixBridge decl_use
V in IndisputableMonolith.RRF.Core.Glossary decl_use
MatrixBridge in IndisputableMonolith.YM.Kernel decl_use
MatrixView in IndisputableMonolith.YM.Kernel decl_use
TransferKernel in IndisputableMonolith.YM.Kernel decl_use