lemma proved term proof

`kernelAtRefK_eq`

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

formal statement (Lean)

  86@[simp] lemma kernelAtRefK_eq (P : KernelParams) (a : ℝ) :
  87    kernelAtRefK P a = kernel P 1 a := by

Term-mode proof.

  88  simp [kernelAtRefK, kernel, one_mul]
  89
  90/-! ## Basic Properties -/
  91
  92/-- Kernel is always positive for valid parameters. -/

Lean names referenced from this declaration's body.

kernel in IndisputableMonolith.Cosmology.BITKernelFamilies decl_use
one_mul in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
kernel in IndisputableMonolith.ILG.Kernel decl_use
kernelAtRefK in IndisputableMonolith.ILG.Kernel decl_use
KernelParams in IndisputableMonolith.ILG.Kernel decl_use
Kernel in IndisputableMonolith.ILG.PressureForm decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
Kernel in IndisputableMonolith.YM.OS decl_use