eval_polynomialZ — Mathlib

English

For any P, the evaluation of the Z-polynomial at P equals a combination of a1-a6 terms with X, Y, Z values at P.

Русский

Для данного P вычисление Z-полином по P даёт линейную комбинацию членов a1…a6, зависящих от X, Y, Z на P.

LaTeX

$$$ \\operatorname{eval} P\\,W'.polynomialZ = W'.a_1 \\cdot P x \\cdot P y + 3 \\cdot W'.a_3 \\cdot P y \\cdot P z^{2} - \\left( 2 \\cdot W'.a_2 \\cdot P x^{2} \\cdot P z + 4 \\cdot W'.a_4 \\cdot P x \\cdot P z^{3} + 6 \\cdot W'.a_6 \\cdot P z^{5} \\right)$$$

Lean4

theorem eval_polynomialZ (P : Fin 3 → R) :
    eval P W'.polynomialZ =
      W'.a₁ * P x * P y + 3 * W'.a₃ * P y * P z ^ 2 -
        (2 * W'.a₂ * P x ^ 2 * P z + 4 * W'.a₄ * P x * P z ^ 3 + 6 * W'.a₆ * P z ^ 5) :=
  by
  rw [polynomialZ_eq]
  simp

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