theorem proved term proof

`rest_energy_is_mass`

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

formal statement (Lean)

 299theorem rest_energy_is_mass (m : ℝ) :
 300    m ^ 2 = 0 ^ 2 + 0 ^ 2 + 0 ^ 2 + m ^ 2 := by ring

Term-mode proof.

 301
 302/-- **Massless particles travel at c**: E = |p| when m = 0. -/

Lean names referenced from this declaration's body.