addXYZ_of_Z_eq_zero_right — Mathlib

English

If Q_z = 0, then W'.addXYZ P Q equals −(Q_x P_z) · P

Русский

Если z-координата Q равна нулю, тогда W'.addXYZ P Q = −(Q_x P_z) · P

LaTeX

$$$$ \\operatorname{addXYZ}(P,Q) = -(Q_x P_z) \\cdot P $$$$

Lean4

theorem addXYZ_of_Z_eq_zero_right {P Q : Fin 3 → R} (hQ : W'.Equation Q) (hQz : Q z = 0) :
    W'.addXYZ P Q = -(Q x * P z) • P := by
  rw [addXYZ, addX_of_Z_eq_zero_right hQz, addY_of_Z_eq_zero_right hQ hQz, addZ_of_Z_eq_zero_right hQz, smul_fin3]

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