theorem proved term proof

`regge_linearity`

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

formal statement (Lean)

  75theorem regge_linearity (r : ℕ) (n₁ n₂ : ℕ) :
  76    regge_mass_squared r (n₁ + n₂) pdg_regge_slope =
  77    regge_mass_squared r n₁ pdg_regge_slope + regge_mass_squared r n₂ pdg_regge_slope := by

proof body

Term-mode proof.

  78  simp [regge_mass_squared]
  79  ring
  80
  81end Physics
  82end IndisputableMonolith

depends on (2)

Lean names referenced from this declaration's body.

pdg_regge_slope in IndisputableMonolith.Physics.Hadrons decl_use
regge_mass_squared in IndisputableMonolith.Physics.Hadrons decl_use