toCharThreeNF_spec — Mathlib

English

There is a CharThreeNF specification for any Weierstrass curve W, determined by whether b₂ is zero or nonzero.

Русский

Для любой кривой Вейерштрасса W существует спецификация CharThreeNF, зависящая от того, равен ли коэффициент b₂ нулю или нет.

LaTeX

$$$\forall {F} [\operatorname{Field} F] (W : \mathrm{WeierstrassCurve} F),\ (W.toCharThreeNF \cdot W).IsCharThreeNF$$$

Lean4

instance toCharThreeNF_spec : (W.toCharThreeNF • W).IsCharThreeNF :=
  by
  by_cases hb₂ : W.b₂ = 0
  · haveI := W.toCharThreeNF_spec_of_b₂_eq_zero hb₂
    infer_instance
  · haveI := W.toCharThreeNF_spec_of_b₂_ne_zero hb₂
    infer_instance

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