inductive definition def or abbrev

`KernelFamily`

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

formal statement (Lean)

  30inductive KernelFamily where
  31  | constant_kernel
  32  | inv_one_plus_z
  33  | exponential
  34  deriving DecidableEq, Inhabited
  35
  36namespace KernelFamily
  37

used by (9)

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

BITKernelFamiliesCert in IndisputableMonolith.Cosmology.BITKernelFamilies decl_use
constant_kernel_eq_one in IndisputableMonolith.Cosmology.BITKernelFamilies decl_use
exp_kernel_pos in IndisputableMonolith.Cosmology.BITKernelFamilies decl_use
inv_one_plus_z_pos in IndisputableMonolith.Cosmology.BITKernelFamilies decl_use
kernel in IndisputableMonolith.Cosmology.BITKernelFamilies decl_use
kernel_at_zero in IndisputableMonolith.Cosmology.BITKernelFamilies decl_use
name in IndisputableMonolith.Cosmology.BITKernelFamilies decl_use
w_eff in IndisputableMonolith.Cosmology.BITKernelFamilies decl_use
w_eff_at_zero in IndisputableMonolith.Cosmology.BITKernelFamilies decl_use