toCharTwoJNeZeroNF — Mathlib

English

Under char-two-zero-normal-form in characteristic two, c4 = 0.

Русский

При характеристике 2 и нормальной форме charTwoJEqZeroNF, c4 = 0.

LaTeX

$$$W.c_4 = 0$$$

Lean4

/-- For a `WeierstrassCurve` defined over a field of characteristic = 2,
there is an explicit change of variables of it to `Y² + XY = X³ + a₂X² + a₆`
(`WeierstrassCurve.IsCharTwoJNeZeroNF`) if its j ≠ 0. -/
def toCharTwoJNeZeroNF (W : WeierstrassCurve F) (ha₁ : W.a₁ ≠ 0) : VariableChange F :=
  ⟨Units.mk0 _ ha₁, W.a₃ / W.a₁, 0, (W.a₁ ^ 2 * W.a₄ + W.a₃ ^ 2) / W.a₁ ^ 3⟩

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