Theorems · Theorem · algebraic geometry

WeierstrassCurve.exists_variableChange_of_j_eq

∀ {F : Type u_1} [inst : Field F] [IsSepClosed F] (E E' : WeierstrassCurve F) [inst_2 : E.IsElliptic]
  [inst_3 : E'.IsElliptic], E.j = E'.j → ∃ C, C • E = E'

If there are two elliptic curves with the same j-invariants defined over a separably closed field, then there exists a change of variables over that field which change one curve into another.

Defined in

Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ

Cited by

0 results in Mathlib

Foundations

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

Assumes

FieldIsSepClosedWeierstrassCurve.IsEllipticWeierstrassCurve.IsElliptic