Theorems · Definition · algebraic geometry

WeierstrassCurve.Projective.polynomial

{R : Type r} → [inst : CommRing R] → WeierstrassCurve.Projective R → MvPolynomial (Fin 3) R

The polynomial W(X, Y, Z) := Y²Z + a₁XYZ + a₃YZ² - (X³ + a₂X²Z + a₄XZ² + a₆Z³) associated to a Weierstrass curve W over a ring R in projective coordinates. This is represented as a term of type MvPolynomial (Fin 3) R, where X, Y, and Z represent X, Y, and Z respectively.

Defined in

Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Cited by

10 results in Mathlib

Foundations

Depth 84 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRing