Y_sub_Y_add_Y_sub_negY — Mathlib

English

P_y Q_z = W.negY Q P_z iff P_y/P_z = W.toAffine.negY(Q_x/Q_z, Q_y/Q_z).

Русский

P_y/Q_z = W.negY Q P_z тогда и только тогда, когда P_y/P_z = W.toAffine.negY(Q_x/Q_z, Q_y/Q_z).

LaTeX

$$$ P_y Q_z = W'.negY Q P_z \\;\\iff\\; \\frac{P_y}{P_z} = W'.toAffine.negY\\left(\\frac{Q_x}{Q_z},\\;\\frac{Q_y}{Q_z}\\right) $$$

Lean4

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

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