eval_polynomialX — Mathlib

English

The value of the X-derivative polynomial evaluated on P equals a linear combination of the affine coordinates with the invariants a1 and a3, namely: 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 равно линейной комбинации аффинных координат с инвариантами a1 и a3: 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_polynomialX (P : Fin 3 → R) :
    eval P W'.polynomialX = W'.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W'.a₂ * P x * P z + W'.a₄ * P z ^ 2) :=
  by
  rw [polynomialX_eq]
  simp

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