a₁_of_isCharNeTwoNF

Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

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

English

If the base ring has characteristic not equal to 2, then the coefficient a1 equals 0.

Русский

Если характеристика базы не равна 2, то коэффициент a1 равен 0.

LaTeX

$$$$ a_1 = 0 $$$$

Lean4

@[simp]
theorem a₁_of_isCharNeTwoNF : W.a₁ = 0 :=
  IsCharNeTwoNF.a₁

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

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

Разделы

Аффилиация

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