Theorem: C06S01.Point.smul_distrib (MIL/C06_Structures/S01_Structures.lean)

State before:
r : ℝ
a b : Point
⊢ (smul r a).add (smul r b) = smul r (a.add b)
Tactic:
simp [add, smul, mul_add]
State after:
no goals