a₂_of_isCharTwoJEqZeroNF

Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

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

English

In the same setting, the coefficient a2 vanishes: a2 = 0.

Русский

В той же конфигурации коэффициент a2 обнулён: a2 = 0.

LaTeX

$$$W.a_2 = 0$$$

Lean4

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

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

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

Разделы

Аффилиация

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