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

State before:
r : ℝ
a b : Point
⊢ add (smul r a) (smul r b) = smul r (add a b)
Tactic:
sorry
State after:
no goals