isCharNeTwoNF_of_isCharThreeNF — Mathlib

English

Let W be a Weierstrass curve over a commutative ring R. If W satisfies CharThreeNF, then W satisfies CharNeTwoNF.

Русский

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

LaTeX

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

Lean4

instance isCharNeTwoNF_of_isCharThreeNF [W.IsCharThreeNF] : W.IsCharNeTwoNF := by
  cases ‹W.IsCharThreeNF› <;> infer_instance

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