polynomialY — Mathlib

English

The nonsingularity criterion interacts with the basis via a map between equations and the basis-based formulation.

Русский

Связь невырожденности с базисом выражается через отображение между уравнениями и базисной формулировкой.

LaTeX

$$nonsingular_iff_variableChange : W.Nonsingular x y ↔ (VariableChange.mk 1 x 0 y • W).toAffine.Nonsingular 0 0$$

Lean4

/-- The partial derivative `W_Y(X, Y)` with respect to `Y` of the polynomial `W(X, Y)` associated to
a Weierstrass curve `W` in affine coordinates. -/
-- TODO: define this in terms of `Polynomial.derivative`.

noncomputable def polynomialY : R[X][Y] :=
  C (C 2) * Y + C (C W.a₁ * X + C W.a₃)

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