b₂_of_isCharNeTwoNF

Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

URI: https://scilib.ai/kg/mathlib#WeierstrassCurve.b₂_of_isCharNeTwoNF

English

If the base ring has characteristic not equal to 2, then the coefficient b2 equals 4 times a2.

Русский

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

LaTeX

$$$$ b_2 = 4 \cdot a_2 $$$$

Lean4

@[simp]
theorem b₂_of_isCharNeTwoNF : W.b₂ = 4 * W.a₂ :=
  by
  rw [b₂, a₁_of_isCharNeTwoNF]
  ring1

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

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

Разделы

Аффилиация

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