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

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