ILG.ParamsKernel
IndisputableMonolith.ILG.ParamsKernel
No prose has been written for this declaration yet. The Lean source and graph data below render without it.
generate prose now
From the project-wide theorem graph. These declarations reference this one in their body.
IndisputableMonolith.ILG.NOfRMono
Lean names referenced from this declaration's body.
IndisputableMonolith.ILG.Params
ParamsKernelVerified
paramsKernel_verified_any