theorem UnitsSystem.Scalar.hMul_assoc [UnitsSystem] {d₁ d₂ d₃ : Dimensions} (a : Scalar d₁) (b : Scalar d₂) (c : Scalar d₃) : a * (b * c) = (a * b * c).cast ⋯

A cast is needed here because (d₁+d₂)+d₃ is not definitionally equal to d₁+(d₂+d₃).

theorem UnitsSystem.Scalar.left_distrib [UnitsSystem] {d₁ d₂ : Dimensions} (a : Scalar d₁) (b c : Scalar d₂) : a * (b + c) = a * b + a * c

theorem UnitsSystem.Scalar.right_distrib [UnitsSystem] {d₁ d₂ : Dimensions} (a b : Scalar d₁) (c : Scalar d₂) : (a + b) * c = a * c + b * c

theorem UnitsSystem.Scalar.sq_add [UnitsSystem] {d : Dimensions} (a b : Scalar d) : (a + b)**2 = a**2 + (2 • a * b).cast ⋯ + b**2

A cast is needed here because 2 • d is not definitionally equal to d+d.

theorem UnitsSystem.Scalar.sq_add' [UnitsSystem] {d : Dimensions} (a b : Scalar d) : (a + b)**2 = a**2 + (2 • a * b).cast ⋯ + b**2

An alternate proof based on working in coordinates