Y_ne_negY_of_Y_ne — Mathlib

English

If P and Q lie on the Jacobian curve and P_x Q_z^2 = Q_x P_z^2 and P_y Q_z^3 ≠ Q_y P_z^3, then P_y ≠ W'.negY P.

Русский

Пусть P,Q лежат на кривой Якобиана и P_x Q_z^2 = Q_x P_z^2, P_y Q_z^3 ≠ Q_y P_z^3. Тогда P_y ≠ W'.negY P.

LaTeX

$$$W'.Nonsingular(P) \to W'.Equation(P) \to W'.Equation(Q) \to (P_x Q_z^2 = Q_x P_z^2) \to (P_y Q_z^3 ≠ Q_y P_z^3) \Rightarrow P_y \neq W'.negY(P)$$$

Lean4

theorem Y_ne_negY_of_Y_ne [NoZeroDivisors R] {P Q : Fin 3 → R} (hP : W'.Equation P) (hQ : W'.Equation Q)
    (hx : P x * Q z ^ 2 = Q x * P z ^ 2) (hy : P y * Q z ^ 3 ≠ Q y * P z ^ 3) : P y ≠ W'.negY P :=
  by
  have hy' : P y * Q z ^ 3 - W'.negY Q * P z ^ 3 = 0 :=
    (mul_eq_zero.mp <| Y_sub_Y_mul_Y_sub_negY hP hQ hx).resolve_left <| sub_ne_zero_of_ne hy
  contrapose! hy
  linear_combination (norm := ring1) Y_sub_Y_add_Y_sub_negY hx + Q z ^ 3 * hy - hy'

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