eval_polynomialX_of_Z_ne_zero — Mathlib

English

The X-coordinate of a projective point on W' is determined by the derivative polynomial in X, and the relation to the affine coordinates on the Z ≠ 0 chart.

Русский

Координата X проективной точки на W' определяется через производный по X многочлен и связь с афинными координатами на диаграмме Z ≠ 0.

LaTeX

$$Relation between X-derivative and projective coordinates$$

Lean4

theorem eval_polynomialX_of_Z_ne_zero {P : Fin 3 → F} (hPz : P z ≠ 0) :
    eval P W.polynomialX / P z ^ 2 = W.toAffine.polynomialX.evalEval (P x / P z) (P y / P z) := by
  linear_combination (norm := (rw [eval_polynomialX, Affine.evalEval_polynomialX]; ring1))
    W.a₁ * P y / P z * div_self hPz - 2 * W.a₂ * P x / P z * div_self hPz - W.a₄ * div_self (pow_ne_zero 2 hPz)

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