centerMass_neg_left — Mathlib

English

For any finite t and nonzero scalar c, centerMass of (c•w) equals centerMass of w.

Русский

Для любого конечного множества t и ненулевого скаляра c центр массы (c•w) равен центру массы w.

LaTeX

$$$\\text{centerMass}(t, c\\cdot w, z)=\\text{centerMass}(t, w, z)$ при $c\\neq 0$.$$

Lean4

@[simp]
theorem centerMass_neg_left : t.centerMass (-w) z = t.centerMass w z := by simp [centerMass, inv_neg]

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