a₁_of_isCharTwoJEqZeroNF

Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

URI: https://scilib.ai/kg/mathlib#WeierstrassCurve.a₁_of_isCharTwoJEqZeroNF

English

In characteristic two nonzero-normal form, the coefficient a1 vanishes: a1 = 0.

Русский

В характеристике двух коэффициент a1 обнулён: a1 = 0.

LaTeX

$$$W.a_1 = 0$$$

Lean4

@[simp]
theorem a₁_of_isCharTwoJEqZeroNF : W.a₁ = 0 :=
  IsCharTwoJEqZeroNF.a₁

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

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

Разделы

Аффилиация

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