eval_polynomialX — Mathlib

English

For any map P: Fin 3 → R, evaluating polynomialX along P matches the Weierstrass Jacobian expression for the same P.

Русский

Для любой функции P: Fin 3 → R, вычисление polynomialX по P совпадает с выражением Вейерштрасс-Джалеков для того же P.

LaTeX

$$$$\operatorname{eval} P\, W'.polynomialX = W'.a_1 \cdot P(y) \cdot P(z) - \bigl( 3 \cdot P(x)^2 + 2 W'.a_2 \cdot P(x) \cdot P(z)^2 + W'.a_4 \cdot P(z)^4 \bigr).$$$$

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 ^ 2 + W'.a₄ * P z ^ 4) :=
  by
  rw [polynomialX_eq]
  simp

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