Theorems · Definition · algebraic geometry

WeierstrassCurve.toCharNeTwoNF

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

There is an explicit change of variables of a WeierstrassCurve to a normal form of characteristic ≠ 2, provided that 2 is invertible in the ring.

Defined in

Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Cited by

6 results in Mathlib

Foundations

Depth 19 from the axioms · uses propext

Assumes

CommRingInvertible