add_of_Z_eq_zero_left — Mathlib

English

If P and Q are nonsingular and P_2 = Q_2 = 0, then W.add P Q equals P y^4 times a fixed vector corresponding to [0,1,0].

Русский

Если P и Q несингулярны и обе P_2 и Q_2 равны нулю, то W.add P Q равен P_y^4 умножить на фиксированный вектор, соответствующий [0,1,0].

LaTeX

$$$ W.add P Q = P_y^4 \\cdot \\llbracket 0,1,0 \\rrbracket $$$

Lean4

theorem add_of_Z_eq_zero_left [NoZeroDivisors R] {P Q : Fin 3 → R} (hP : W'.Equation P) (hPz : P z = 0)
    (hQz : Q z ≠ 0) : W'.add P Q = (P y ^ 2 * Q z) • Q := by
  rw [add_of_not_equiv <| not_equiv_of_Z_eq_zero_left hPz hQz, addXYZ_of_Z_eq_zero_left hP hPz]

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