eval_polynomial_of_Z_ne_zero — Mathlib

English

If P z ≠ 0, dividing the Jacobian polynomial by P z^6 yields the evaluation of the affine polynomial of W at the normalized coordinates P_x/P_z^2 and P_y/P_z^3.

Русский

Если P_z ≠ 0, деление полинома Жакобиана на P_z^6 даёт значение аффинного полинома W в нормализованных координатах P_x/P_z^2 и P_y/P_z^3.

LaTeX

$$eval P W.polynomial / P_z^6 = W.toAffine.polynomial.evalEval (P_x/P_z^2) (P_y/P_z^3)$$

Lean4

theorem eval_polynomial_of_Z_ne_zero {P : Fin 3 → F} (hPz : P z ≠ 0) :
    eval P W.polynomial / P z ^ 6 = W.toAffine.polynomial.evalEval (P x / P z ^ 2) (P y / P z ^ 3) := by
  linear_combination (norm := (rw [eval_polynomial, Affine.evalEval_polynomial]; ring1))
    W.a₁ * P x * P y / P z ^ 5 * div_self hPz + W.a₃ * P y / P z ^ 3 * div_self (pow_ne_zero 3 hPz) -
          W.a₂ * P x ^ 2 / P z ^ 4 * div_self (pow_ne_zero 2 hPz) -
        W.a₄ * P x / P z ^ 2 * div_self (pow_ne_zero 4 hPz) -
      W.a₆ * div_self (pow_ne_zero 6 hPz)

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