Equation — Mathlib

English

The projective point lies on W' iff the homogeneous polynomial evaluates to zero at its homogeneous coordinates.

Русский

Предикат Equation(P) означает, что проективная точка P = (P x, P y, P z) лежит на кривой Вейерштрасса W'. Другими словами, выполняется однородное уравнение Вейерштрасса W'(X, Y, Z) = 0.

LaTeX

$$$W'.Equation(P) \\;\\;\\text{ означает }\\;\\; W'.polynomial(P) = 0$$$

Lean4

/-- The proposition that a projective point representative `(x, y, z)` lies in a Weierstrass curve
`W`.

In other words, it satisfies the homogeneous Weierstrass equation `W(X, Y, Z) = 0`. -/
def Equation (P : Fin 3 → R) : Prop :=
  eval P W'.polynomial = 0

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