addXYZ_neg — Mathlib

English

The sum of P and its negation under addXYZ equals the negated scalar times the vector [1,1,0].

Русский

Сумма P и его отрицания под addXYZ равна отрицательному скалярному умножению на вектор [1,1,0].

LaTeX

$$$\forall {P : \mathrm{Fin}_3 \to R},\ W'.Equation P \Rightarrow W'.addXYZ P (W'.neg P) = -W'.\mathrm{dblZ} P \cdot \![1, 1, 0]$$$

Lean4

theorem addXYZ_neg {P : Fin 3 → R} (hP : W'.Equation P) : W'.addXYZ P (W'.neg P) = -W'.dblZ P • ![1, 1, 0] := by
  erw [addXYZ, addX_neg hP, addY_neg hP, addZ_neg, smul_fin3, neg_sq, mul_one, Odd.neg_pow <| by decide, mul_one,
    mul_zero]

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