c₆_of_isCharTwoJEqZeroNF

Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

URI: https://scilib.ai/kg/mathlib#WeierstrassCurve.c₆_of_isCharTwoJEqZeroNF

English

The invariant c6 equals minus two hundred sixteen times b6: c6 = -216 b6.

Русский

Инвариант c6 равен минус 216 от b6: c6 = -216 b6.

LaTeX

$$$W.c_6 = -216 \; W.b_6$$$

Lean4

@[simp]
theorem c₆_of_isCharTwoJEqZeroNF : W.c₆ = -216 * W.b₆ :=
  by
  rw [c₆, b₂_of_isCharTwoJEqZeroNF, b₄_of_isCharTwoJEqZeroNF]
  ring1

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

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

Разделы

Аффилиация

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