isCharTwoNF_of_isCharTwoJNeZeroNF

Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

URI: https://scilib.ai/kg/mathlib#WeierstrassCurve.isCharTwoNF_of_isCharTwoJNeZeroNF

English

If j ≠ 0, then the curve has CharTwoNF, i.e., there exists a normal form in char 2.

Русский

Если j ≠ 0, то кривая имеет CharTwoNF, то есть существует обобщённая нормальная форма в характеристике 2.

LaTeX

$$$W.IsCharTwoNF$$$

Lean4

instance isCharTwoNF_of_isCharTwoJNeZeroNF [W.IsCharTwoJNeZeroNF] : W.IsCharTwoNF :=
  IsCharTwoNF.of_j_ne_zero

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru