addZ_eq' — Mathlib

English

If P_z = 0, then addZ(P,Q) = P_y^4 · [0,1,0].

Русский

Если P_z = 0, то addZ(P,Q) = P_y^4 · [0,1,0].

LaTeX

$$$P_z = 0 \Rightarrow W'.addZ(P,Q) = P_y^4 \cdot \begin{bmatrix}0\\1\\0\end{bmatrix}$$$

Lean4

theorem addZ_eq' {P Q : Fin 3 → R} (hP : W'.Equation P) (hQ : W'.Equation Q) :
    W'.addZ P Q * (P z * Q z) = (P x * Q z - Q x * P z) ^ 3 := by
  linear_combination (norm := (rw [addZ]; ring1)) Q z ^ 3 * (equation_iff _).mp hP - P z ^ 3 * (equation_iff _).mp hQ

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