addX_eq — Mathlib

English

The equality addX_eq expresses addX in terms of the affine coordinates when the Z's are nonzero.

Русский

Равенство addX_eq выражает addX через аффинные координаты при ненулевых Z.

LaTeX

$$W'.addX P Q = ( (P y Q z^3 - Q y P z^3)^2 + ... ) / (P z Q z)^2$$

Lean4

theorem addX_eq {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P z ≠ 0) (hQz : Q z ≠ 0) :
    W.addX P Q =
      ((P y * Q z ^ 3 - Q y * P z ^ 3) ^ 2 + W.a₁ * (P y * Q z ^ 3 - Q y * P z ^ 3) * P z * Q z * addZ P Q -
              W.a₂ * P z ^ 2 * Q z ^ 2 * addZ P Q ^ 2 -
            P x * Q z ^ 2 * addZ P Q ^ 2 -
          Q x * P z ^ 2 * addZ P Q ^ 2) /
        (P z * Q z) ^ 2 :=
  by rw [← addX_eq' hP hQ, mul_div_cancel_right₀ _ <| pow_ne_zero 2 <| mul_ne_zero hPz hQz]

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