negAddY_of_Z_eq_zero_right — Mathlib

English

If W'.Equation Q and Q z = 0, then W'.negAddY P Q = (-(Q x * P z))^3 * W'.negY P.

Русский

Если W'.Equation Q и Q z = 0, то W'.negAddY P Q = (-(Q x * P z))^3 * W'.negY P.

LaTeX

$$W'.Equation Q ∧ Q z = 0 ⇒ W'.negAddY P Q = (-(Q x * P z))^3 · W'.negY P.$$

Lean4

theorem negAddY_of_Z_eq_zero_right {P Q : Fin 3 → R} (hQ : W'.Equation Q) (hQz : Q z = 0) :
    W'.negAddY P Q = (-(Q x * P z)) ^ 3 * W'.negY P := by
  linear_combination (norm := (rw [negAddY, negY, hQz]; ring1))
    (P y - W'.negY P) * P z ^ 3 * (equation_of_Z_eq_zero hQz).mp hQ

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