Y_eq_of_Y_ne' — Mathlib

English

If two points P and Q on the curve satisfy hx and the Y-values are not both zero, then P_y Q_z = negY Q P_z.

Русский

Если две точки P и Q на кривой удовлетворяют hx и значения Y не равны нулю, тогда P_y Q_z = negY Q P_z.

LaTeX

$$$ P_y Q_z = W'.negY Q P_z $$$

Lean4

theorem Y_eq_of_Y_ne' [NoZeroDivisors R] {P Q : Fin 3 → R} (hP : W'.Equation P) (hQ : W'.Equation Q) (hPz : P z ≠ 0)
    (hQz : Q z ≠ 0) (hx : P x * Q z = Q x * P z) (hy : P y * Q z ≠ W'.negY Q * P z) : P y * Q z = Q y * P z :=
  sub_eq_zero.mp <|
    (mul_eq_zero.mp <|
          (mul_eq_zero.mp <| Y_sub_Y_mul_Y_sub_negY hP hQ hx).resolve_right <| sub_ne_zero.mpr hy).resolve_left <|
      mul_ne_zero hPz hQz

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