negAddY_neg — Mathlib

English

The negAddY operation on P and W'.neg P yields (dblZ P)^3.

Русский

Операция negAddY на P и W'.neg P дает (dblZ P)^3.

LaTeX

$$$\forall {P : \mathrm{Fin}_3 \to R},\ W'.Equation P \Rightarrow W'.negAddY P (W'.neg P) = (W'.dblZ P)^3$$$

Lean4

theorem negAddY_neg {P : Fin 3 → R} (hP : W'.Equation P) : W'.negAddY P (W'.neg P) = W'.dblZ P ^ 3 := by
  linear_combination (norm := (rw [negAddY, neg_X, neg_Y, neg_Z, dblZ, negY]; ring1))
    -2 * P z ^ 3 * (P y - W'.negY P) * (equation_iff _).mp hP

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