eval_polynomialY_of_Z_ne_zero — Mathlib

English

The evaluation of polynomialX on P yields the same combination as in the explicit formula for X, i.e., eval P W'.polynomialX = a1 P y P z − (3 P x^2 + 2 a2 P x P z + a4 P z^2).

Русский

Значение polynomialX на P равно той же комбинации мономов, что и формула для X: eval P W'.polynomialX = a1 P y P z − (3 P x^2 + 2 a2 P x P z + a4 P z^2).

LaTeX

$$$\\mathrm{eval}\\;P\\;W'.polynomialX = W'.a_1 \\cdot P y \\cdot P z - (3 \\cdot P x^{2} + 2 \\cdot W'.a_2 \\cdot P x \\cdot P z + W'.a_4 \\cdot P z^{2})$$$

Lean4

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

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