centerMass_smul_left — Mathlib

English

If the weights sum to 1, the centerMass equals the weighted sum ∑ w_i z_i.

Русский

Если веса суммируются к 1, центр массы равен взвешенной сумме точек: ∑ w_i z_i.

LaTeX

$$$\\sum_{i\\in t} w_i = 1 \\Rightarrow t.centerMass w z = \\sum_{i\\in t} w_i \\cdot z_i.$$$

Lean4

theorem centerMass_smul_left {c : R'} [Module R' R] [Module R' E] [SMulCommClass R' R R] [IsScalarTower R' R R]
    [SMulCommClass R R' E] [IsScalarTower R' R E] (hc : c ≠ 0) : t.centerMass (c • w) z = t.centerMass w z := by
  simp [centerMass, -smul_assoc, smul_assoc c, ← smul_sum, smul_inv₀, smul_smul_smul_comm, hc]

Похожие утверждения