Theorems · Definition · algebraic geometry

WeierstrassCurve.toShortNFOfCharThree

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

For a WeierstrassCurve defined over a ring of characteristic = 3, there is an explicit change of variables of it to Y² = X³ + a₄X + a₆ (WeierstrassCurve.IsShortNF) if its j = 0. This is in fact given by WeierstrassCurve.toCharNeTwoNF.

Defined in

Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Cited by

5 results in Mathlib

Foundations

Depth 25 from the axioms · uses propext

Assumes

CommRingCharP