polynomialX — Mathlib

English

In general, nonsingularity at a point (x,y) is governed by the equation together with a nonzero condition on certain linear/quadratic expressions in x,y involving the coefficients a1,a2,a3,a4.

Русский

Общее условие невырожденности в точке (x,y) задаётся уравнением вместе с ненулевостью некоторых линейных/квадратичных выражений в x,y и коэффициентах a1,a2,a3,a4.

LaTeX

$$W.Nonsingular x y ↔ W.Equation x y ∧ (W.a₁ * y ≠ 3 * x^2 + 2 * W.a₂ * x + W.a₄ ∨ y ≠ -y - W.a₁ * x - W.a₃)$$

Lean4

/-- The partial derivative `W_X(X, Y)` with respect to `X` 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 polynomialX : R[X][Y] :=
  C (C W.a₁) * Y - C (C 3 * X ^ 2 + C (2 * W.a₂) * X + C W.a₄)

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