theorem
proved
term proof
energy_momentum_relation
show as:
view Lean formalization →
formal statement (Lean)
294theorem energy_momentum_relation (E p₁ p₂ p₃ m : ℝ)
295 (h : E ^ 2 = p₁ ^ 2 + p₂ ^ 2 + p₃ ^ 2 + m ^ 2) :
296 E ^ 2 - (p₁ ^ 2 + p₂ ^ 2 + p₃ ^ 2) = m ^ 2 := by linarith
proof body
Term-mode proof.
297
298/-- **Rest energy = rest mass** (in natural units c = 1). -/