toCharNeTwoNF — Mathlib

English

There is an explicit linear change of variables of a Weierstrass curve to a normal form for characteristic not equal to 2, provided that 2 is invertible in the ring.

Русский

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

LaTeX

$$$$ \text{toCharNeTwoNF} : \text{WeierstrassCurve} \; R \to \text{VariableChange } R \text{ (при обратимости } 2) $$$$

Lean4

/-- 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. -/
@[simps]
def toCharNeTwoNF : VariableChange R :=
  ⟨1, 0, ⅟2 * -W.a₁, ⅟2 * -W.a₃⟩

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