polynomial — Mathlib

Lean4
/-- The polynomial `W(X, Y) := Y² + a₁XY + a₃Y - (X³ + a₂X² + a₄X + a₆)` associated to a Weierstrass
curve `W` over a ring `R` in affine coordinates.

For ease of polynomial manipulation, this is represented as a term of type `R[X][X]`, where the
inner variable represents `X` and the outer variable represents `Y`. For clarity, the alternative
notations `Y` and `R[X][Y]` are provided in the `Polynomial.Bivariate` scope to represent the outer
variable and the bivariate polynomial ring `R[X][X]` respectively. -/
noncomputable def polynomial : R[X][Y] :=
  Y ^ 2 + C (C W.a₁ * X + C W.a₃) * Y - C (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)
Похожие утверждения