add_of_Y_eq — Mathlib

English

With P and Q nonsingular and P_z ≠ 0, Q_z = 0, then W.add P Q equals −(Q_y^2 * P_z) • P under suitable hypotheses.

Русский

При несингулярности P и Q и P_z ≠ 0, Q_z = 0, то W.add P Q равно −(Q_y^2 * P_z) • P при заданных условиях.

LaTeX

$$$ W.add P Q = - \\left(Q_y^2 \\cdot P_z\\right) \\cdot P $$$

Lean4

theorem add_of_Y_eq {P Q : Fin 3 → F} (hP : W.Equation P) (hPz : P z ≠ 0) (hQz : Q z ≠ 0) (hx : P x * Q z = Q x * P z)
    (hy : P y * Q z = Q y * P z) (hy' : P y * Q z = W.negY Q * P z) : W.add P Q = W.dblU P • ![0, 1, 0] := by
  rw [add_of_equiv <| equiv_of_X_eq_of_Y_eq hPz hQz hx hy, dblXYZ_of_Y_eq hP hPz hQz hx hy hy']

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