polynomial — Mathlib

English

If P z ≠ 0, then P is equivalent to a canonical representative with z=1, as above.

Русский

Если P_z ≠ 0, то P эквивалентно каноническому представителю с z=1.

LaTeX

$$If $P_z\neq 0$, then $P \approx ![P_x/P_z^2, P_y/P_z^3, 1]$$$

Lean4

/-- The polynomial `W(X, Y, Z) := Y² + a₁XYZ + a₃YZ³ - (X³ + a₂X²Z² + a₄XZ⁴ + a₆Z⁶)` associated to a
Weierstrass curve `W` over a ring `R` in Jacobian coordinates.

This is represented as a term of type `MvPolynomial (Fin 3) R`, where `X`, `Y`, and `Z`
represent `X`, `Y`, and `Z` respectively. -/
noncomputable def polynomial : MvPolynomial (Fin 3) R :=
  Y ^ 2 + C W'.a₁ * X * Y * Z + C W'.a₃ * Y * Z ^ 3 -
    (X ^ 3 + C W'.a₂ * X ^ 2 * Z ^ 2 + C W'.a₄ * X * Z ^ 4 + C W'.a₆ * Z ^ 6)

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