Theorems · Definition · algebraic geometry

WeierstrassCurve.j

{R : Type u} → [inst : CommRing R] → (W : WeierstrassCurve R) → [W.IsElliptic] → R

The j-invariant j of an elliptic curve, which is invariant under isomorphisms over R. Note that to prove two equal elliptic curves have the same j, you need to use simp_rw, as rw cannot transfer instance WeierstrassCurve.IsElliptic automatically.

Defined in

Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass

Cited by

27 results in Mathlib

Foundations

Depth 24 from the axioms · uses propext, Classical.choice

Assumes

CommRingWeierstrassCurve.IsElliptic