def definition def or abbrev

`ParamsKernelVerified`

show as: view Lean formalization →

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)

   8def ParamsKernelVerified (P : Params) : Prop :=

proof body

Definition body.

   9  ParamProps P
  10

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

paramsKernel_verified_any in IndisputableMonolith.ILG.ParamsKernel decl_use

depends on (7)

Lean names referenced from this declaration's body.

ParamProps in IndisputableMonolith.Gravity.ILG decl_use
Params in IndisputableMonolith.Gravity.ILG decl_use
ParamProps in IndisputableMonolith.ILG.Params decl_use
Params in IndisputableMonolith.ILG.Params decl_use
ParamProps in IndisputableMonolith.Relativity.ILG.Params decl_use
Params in IndisputableMonolith.Relativity.ILG.Params decl_use
Params in IndisputableMonolith.Spiral.SpiralField decl_use