toShortNF — Mathlib

English

There is an explicit change of variables that transforms a Weierstrass curve into a short normal form, assuming 2 and 3 are invertible.

Русский

Существуют явное изменение переменных, переводящее кривую Вейерштрасса к краткой нормальной форме, при условии обратимости 2 и 3.

LaTeX

$$$ \exists C:\mathrm{VariableChange}(R),\ (C\cdot W)\text{ is in short normal form} $$$

Lean4

/-- 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`. -/
def toShortNF : VariableChange R :=
  ⟨1, ⅟3 * -(W.toCharNeTwoNF • W).a₂, 0, 0⟩ * W.toCharNeTwoNF

Похожие утверждения