Y_sub_Y_add_Y_sub_negY — Mathlib

English

For P,Q in Fin 3 → R, the identity (P_y Q_z^3 − Q_y P_z^3) + (P_y Q_z^3 − W'.negY Q P_z^3) = (P_y − W'.negY P) Q_z^3 holds, expressing a standard linear combination relating Y-coordinates.

Русский

Для P,Q в Fin(3)→R верна тождественность (P_y Q_z^3 − Q_y P_z^3) + (P_y Q_z^3 − W'.negY Q P_z^3) = (P_y − W'.negY P) Q_z^3, выражающая обычную линейную комбинацию по Y-координатам.

LaTeX

$$$(P_1 Q_2^3 - Q_1 P_2^3) + (P_1 Q_2^3 - W'.negY(Q) P_2^3) = (P_1 - W'.negY(P)) Q_2^3$$$

Lean4

theorem Y_sub_Y_add_Y_sub_negY {P Q : Fin 3 → R} (hx : P x * Q z ^ 2 = Q x * P z ^ 2) :
    (P y * Q z ^ 3 - Q y * P z ^ 3) + (P y * Q z ^ 3 - W'.negY Q * P z ^ 3) = (P y - W'.negY P) * Q z ^ 3 := by
  linear_combination (norm := (rw [negY, negY]; ring1)) -W'.a₁ * P z * Q z * hx

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