isCharThreeNF_of_isShortNF — Mathlib

English

Let W be a Weierstrass curve over a commutative ring R. If W is in Short NF, then W has the CharThreeNF property.

Русский

Пусть W — кривая Вейерштрасса над коммутативным кольцом R. Если W находится в форме ShortNF, тогда W обладает свойством CharThreeNF.

LaTeX

$$$\forall {R} [\operatorname{CommRing} R] (W : \mathrm{WeierstrassCurve} R), [W.IsShortNF] \Rightarrow W.IsCharThreeNF$$$

Lean4

instance isCharThreeNF_of_isShortNF [W.IsShortNF] : W.IsCharThreeNF :=
  IsCharThreeNF.of_j_eq_zero

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