toCharTwoJEqZeroNF — Mathlib

English

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

Русский

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

LaTeX

$$$W.b_4 = 0$$$

Lean4

/-- For a `WeierstrassCurve` defined over a ring of characteristic = 2,
there is an explicit change of variables of it to `Y² + a₃Y = X³ + a₄X + a₆`
(`WeierstrassCurve.IsCharTwoJEqZeroNF`) if its j = 0. -/
def toCharTwoJEqZeroNF : VariableChange R :=
  ⟨1, W.a₂, 0, 0⟩

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