pith. machine review for the scientific record. sign in
theorem proved term proof

partialWidth_match

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)

  69theorem partialWidth_match
  70    (amp1 amp2 phaseSpace1 phaseSpace2 : ℝ)
  71    (hamp : amp1 = amp2) (hps : phaseSpace1 = phaseSpace2) :
  72    partialWidth amp1 phaseSpace1 = partialWidth amp2 phaseSpace2 := by

proof body

Term-mode proof.

  73  rw [hamp, hps]
  74
  75/-! ## §2. Total Width and Branching Ratios -/
  76
  77/-- The total Higgs width is the sum of partial widths over all channels.
  78    We model "all channels" as a finite list of `(amp, phaseSpace)` pairs. -/

used by (2)

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

depends on (20)

Lean names referenced from this declaration's body.