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 a3 equals 0.

Русский

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

LaTeX

$$$$ a_3 = 0 $$$$

Lean4

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

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

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

Разделы

Аффилиация

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