theorem proved term proof

`val_smul`

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

formal statement (Lean)

 184@[simp] theorem val_smul {U : Type} (r : ℝ) (a : Quantity U) : (r • a).val = r * a.val := rfl

Term-mode proof.

 185
 186end Quantity
 187
 188/-! ### Unit/semantic tags (empty types) -/
 189

Lean names referenced from this declaration's body.