Theorems · Definition · algebraic geometry

WeierstrassCurve.Affine.CoordinateRing.XYIdeal

{R : Type r} → [inst : CommRing R] → (W' : WeierstrassCurve.Affine R) → R → Polynomial R → Ideal W'.CoordinateRing

The ideal ⟨X - x, Y - y(X)⟩ of R[W] for some x in R and y(X) in R[X].

Defined in

Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Cited by

9 results in Mathlib

Foundations

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

Assumes

CommRing