toCharTwoNF — Mathlib

English

In char-two-zero-normal-form, Δ = a3^4.

Русский

В нормальной форме charTwoJEqZeroNF, Δ = a3^4.

LaTeX

$$$W.\Delta = W.a_3^{4}$$$

Lean4

/-- For a `WeierstrassCurve` defined over a field of characteristic = 2,
there is an explicit change of variables of it to `WeierstrassCurve.IsCharTwoNF`, that is,
`Y² + XY = X³ + a₂X² + a₆` (`WeierstrassCurve.IsCharTwoJNeZeroNF`) or
`Y² + a₃Y = X³ + a₄X + a₆` (`WeierstrassCurve.IsCharTwoJEqZeroNF`). -/
def toCharTwoNF [DecidableEq F] : VariableChange F :=
  if ha₁ : W.a₁ = 0 then W.toCharTwoJEqZeroNF else W.toCharTwoJNeZeroNF ha₁

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