addX_neg — Mathlib

English

If P satisfies the X-equation W'.Equation P, then W'.addX(P, W'.neg P) equals (dblZ P)^2.

Русский

Если P удовлетворяет уравнению X на кривой, то W'.addX(P, W'.neg P) равно (dblZ P)^2.

LaTeX

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

Lean4

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

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