polynomialY — Mathlib

English

If P z ≠ 0, then W.Equation P is equivalent to the affine equation W.toAffine.Equation (P x / P z) (P y / P z).

Русский

Если P z ≠ 0, то W.Equation P эквивалентно афинному уравнению W.toAffine.Equation (P x / P z) (P y / P z).

LaTeX

$$$P z \\neq 0 \\Rightarrow W.Equation P \\iff W.toAffine.Equation( P x / P z , P y / P z )$$$

Lean4

/-- The partial derivative `W_Y(X, Y, Z)` with respect to `Y` of the polynomial `W(X, Y, Z)`
associated to a Weierstrass curve `W` in projective coordinates. -/
noncomputable def polynomialY : MvPolynomial (Fin 3) R :=
  pderiv y W'.polynomial

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