negAddY_eq' — Mathlib

English

A rearranged identity expresses negAddY in terms of addX, addZ and y-coordinates.

Русский

Ещё одно выражение для negAddY через addX, addZ и y-координаты.

LaTeX

$$W'.negAddY P Q * (P z Q z)^3 = (P y Q z^3 - Q y P z^3) * (W'.addX P Q * (P z Q z)^2 - P x Q z^2 * addZ P Q^2) + P y Q z^3 * addZ P Q^3$$

Lean4

theorem negAddY_eq' (P Q : Fin 3 → R) :
    W'.negAddY P Q * (P z * Q z) ^ 3 =
      (P y * Q z ^ 3 - Q y * P z ^ 3) * (W'.addX P Q * (P z * Q z) ^ 2 - P x * Q z ^ 2 * addZ P Q ^ 2) +
        P y * Q z ^ 3 * addZ P Q ^ 3 :=
  by
  rw [negAddY, addX, addZ]
  ring1

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