inductive definition def or abbrev

`DecayChannel`

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

formal statement (Lean)

  18inductive DecayChannel where
  19  | alpha
  20  | betaMinus
  21  | betaPlus
  22  | electronCapture
  23  | spontaneousFission
  24  deriving DecidableEq, Repr, BEq, Fintype
  25

used by (5)

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

decayChannel_count in IndisputableMonolith.Physics.DecaySpectrumFromPhiLadder decl_use
DecaySpectrumCert in IndisputableMonolith.Physics.DecaySpectrumFromPhiLadder decl_use
DecayChannel in IndisputableMonolith.Physics.VacuumDecayFromJCost decl_use
decayChannel_count in IndisputableMonolith.Physics.VacuumDecayFromJCost decl_use
VacuumDecayCert in IndisputableMonolith.Physics.VacuumDecayFromJCost decl_use

depends on (2)

Lean names referenced from this declaration's body.

alpha in IndisputableMonolith.Constants.Alpha decl_use
DecayChannel in IndisputableMonolith.Physics.VacuumDecayFromJCost decl_use