evalEval_polynomial — Mathlib

English

The polynomial attached to a mapped Weierstrass curve equals the mapped polynomial.

Русский

Полином, связанный с отображённой кривой Вейерштрасса, совпадает с отображённым полиномом.

LaTeX

$$(W.map f).toAffine.polynomial = W.polynomial.map (mapRingHom f)$$

Lean4

theorem evalEval_polynomial (x y : R) :
    W.polynomial.evalEval x y = y ^ 2 + W.a₁ * x * y + W.a₃ * y - (x ^ 3 + W.a₂ * x ^ 2 + W.a₄ * x + W.a₆) :=
  by
  simp only [polynomial]
  eval_simp
  rw [add_mul, ← add_assoc]

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