negDblY_of_Y_eq' — Mathlib

English

A formula expressing negDblY P via a long algebraic combination including W'.polynomialX, W'.a1, W'.a2, etc., with P 2 powers and cross-terms in P x, P y, P z.

Русский

Длинная алгебраическая формула для negDblY P через W'.polynomialX и константы кривой, с учетом степеней P 2 и перекрестных членов P_x, P_y, P_z.

LaTeX

$$$ {P: Fin 3 → F} (hP: W'.Equation P) : W'.negDblY P = \cdots$ (с учётом W'.polynomialX и коэффициентов кривой)$$

Lean4

theorem negDblY_of_Y_eq' [NoZeroDivisors R] {P Q : Fin 3 → R} (hP : W'.Equation P) (hQz : Q z ≠ 0)
    (hx : P x * Q z = Q x * P z) (hy : P y * Q z = Q y * P z) (hy' : P y * Q z = W'.negY Q * P z) :
    W'.negDblY P * P z ^ 2 = -eval P W'.polynomialX ^ 3 :=
  by
  rw [negDblY_eq' hP, Y_eq_negY_of_Y_eq hQz hx hy hy']
  ring1

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