eval_polynomialY_of_Z_ne_zero — Mathlib

English

If P z ≠ 0, then the Y-coordinate evaluation divided by P z^3 equals the affine Y-evaluation of the normalized coordinates.

Русский

При P z ≠ 0 деление значения по Z на P z^3 даёт аффинную оценку по нормализованным координатам.

LaTeX

$$$\\operatorname{eval} P\\,W'.polynomialY \\/ P z^{3} = W.toAffine.polynomialY.evalEval (P x / P z^{2}) (P y / P z^{3})$$$

Lean4

theorem eval_polynomialY_of_Z_ne_zero {P : Fin 3 → F} (hPz : P z ≠ 0) :
    eval P W.polynomialY / P z ^ 3 = W.toAffine.polynomialY.evalEval (P x / P z ^ 2) (P y / P z ^ 3) := by
  linear_combination (norm := (rw [eval_polynomialY, Affine.evalEval_polynomialY]; ring1))
    W.a₁ * P x / P z ^ 2 * div_self hPz + W.a₃ * div_self (pow_ne_zero 3 hPz)

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