toCharTwoNF_spec — Mathlib

English

There is a specification that a Weierstrass curve in char 2 has a CharTwoNF form, given whether a1 equals zero or not.

Русский

Существует спецификация, что кривая Вейерштрасса в характеристике 2 имеет форму CharTwoNF, зависящую от равенства a1 нулю или нет.

LaTeX

$$$(W.toCharTwoNF) \; \text{ is defined by cases on } W.a_1 = 0$$$

Lean4

instance toCharTwoNF_spec [DecidableEq F] : (W.toCharTwoNF • W).IsCharTwoNF :=
  by
  by_cases ha₁ : W.a₁ = 0
  · rw [toCharTwoNF, dif_pos ha₁]
    haveI := W.toCharTwoJEqZeroNF_spec ha₁
    infer_instance
  · rw [toCharTwoNF, dif_neg ha₁]
    haveI := W.toCharTwoJNeZeroNF_spec ha₁
    infer_instance

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