Theorems · Definition · algebraic geometry

WeierstrassCurve.toCharThreeNF

{F : Type u_2} → [inst : Field F] → [CharP F 3] → WeierstrassCurve F → WeierstrassCurve.VariableChange F

For a WeierstrassCurve defined over a field of characteristic = 3, there is an explicit change of variables of it to WeierstrassCurve.IsCharThreeNF, that is, Y² = X³ + a₂X² + a₆ (WeierstrassCurve.IsCharThreeJNeZeroNF) or Y² = X³ + a₄X + a₆ (WeierstrassCurve.IsShortNF). It is the composition of an explicit change of variables with WeierstrassCurve.toShortNFOfCharThree.

Defined in

Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Cited by

3 results in Mathlib

Foundations

Depth 45 from the axioms · uses propext, Quot.sound

Assumes

FieldCharP