add_of_Z_eq_zero — Mathlib

English

If P ≈ Q and P z ≠ 0, Q z ≠ 0 and hy holds, then W'.addXYZ P (W'.neg P) equals a vector involving [0,1,0] in the middle slot, specifically -W'.dblZ P • ![0,1,0].

Русский

Если P ≈ Q и P_z ≠ 0, Q_z ≠ 0 и выполняются некие условия, тогда W'.addXYZ P (W'.neg P) равно вектору с центральной составляющей [0,1,0] и скаляру −W'.dblZ P: W'.addXYZ P (W'.neg P) = -W'.dblZ P • ![0,1,0].

LaTeX

$$$ W'.addXYZ P (W'.neg P) = - W'.dblZ P \\cdot ![0,1,0] $$$

Lean4

theorem add_of_Z_eq_zero {P Q : Fin 3 → F} (hP : W.Nonsingular P) (hQ : W.Nonsingular Q) (hPz : P z = 0)
    (hQz : Q z = 0) : W.add P Q = P y ^ 4 • ![0, 1, 0] := by
  rw [add_of_equiv <| equiv_of_Z_eq_zero hP hQ hPz hQz, dblXYZ_of_Z_eq_zero hP.left hPz]

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