English
Let t be a finite index set, w: t → R weights, z: t → E a family of points in a vector space E, and c a scalar. Then multiplying every point by c before taking the center of mass is the same as taking the center of mass first and then multiplying by c.
Русский
Пусть t – конечное множество индексов, w: t → R – веса, z: t → E – семейство точек в векторном пространстве E, и c ∈ R. Тогда центр массы точек c·z_i равен c·(центр массы точек z_i).
LaTeX
$$$ (t.centerMass\, w\, (i \mapsto c \cdot z_i)) = c \cdot (t.centerMass\, w\, z) $$$
Lean4
theorem centerMass_smul : (t.centerMass w fun i => c • z i) = c • t.centerMass w z := by
simp only [Finset.centerMass, Finset.smul_sum, (mul_smul _ _ _).symm, mul_comm c, mul_assoc]
