addXYZ_of_X_eq — Mathlib

English

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

Русский

Если P_z = 0, тогда W'.addXYZ P Q = (P_x Q_z) · Q.

LaTeX

$$$$ \\operatorname{addXYZ}(P,Q) = (P_x Q_z) \\cdot Q $$$$

Lean4

theorem addXYZ_of_X_eq {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P z ≠ 0) (hQz : Q z ≠ 0)
    (hx : P x * Q z ^ 2 = Q x * P z ^ 2) : W.addXYZ P Q = addU P Q • ![1, 1, 0] := by
  erw [addXYZ, addX_of_X_eq hP hQ hPz hQz hx, addY_of_X_eq hP hQ hPz hQz hx, addZ_of_X_eq hx, smul_fin3, mul_one,
    mul_one, mul_zero]

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