isCharTwoNF_of_isCharTwoJEqZeroNF

Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

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

English

If j = 0, then the curve has CharTwoJEqZeroNF (a different normal form).

Русский

Если j = 0, то кривая имеет CharTwoJEqZeroNF (другая нормальная форма).

LaTeX

$$$W.IsCharTwoJEqZeroNF$$$

Lean4

instance isCharTwoNF_of_isCharTwoJEqZeroNF [W.IsCharTwoJEqZeroNF] : W.IsCharTwoNF :=
  IsCharTwoNF.of_j_eq_zero

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

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

Разделы

Аффилиация

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