addY_neg — Mathlib

English

For P with W'.Equation P, addY(P, W'.neg P) equals the negation of the triple product of the cube of dblZ(P).

Русский

Для P с W'.Equation P, addY(P, W'.neg P) равняется отрицанию кубического произведения dblZ(P).

LaTeX

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

Lean4

theorem addY_neg {P : Fin 3 → R} (hP : W'.Equation P) : W'.addY P (W'.neg P) = -W'.dblZ P ^ 3 :=
  by
  rw [addY, addX_neg hP, negAddY_neg hP, addZ_neg, negY_of_Z_eq_zero rfl]
  rfl

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