Theorems · Definition · algebraic geometry

WeierstrassCurve.toShortNF

{R : Type u_1} →
  [inst : CommRing R] → WeierstrassCurve R → [Invertible 2] → [Invertible 3] → WeierstrassCurve.VariableChange R

There is an explicit change of variables of a WeierstrassCurve to a short normal form, provided that 2 and 3 are invertible in the ring. It is the composition of an explicit change of variables with WeierstrassCurve.toCharNeTwoNF.

Defined in

Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Cited by

1 results in Mathlib

Foundations

Depth 20 from the axioms · uses propext

Assumes

CommRingInvertibleInvertible