c₄_of_isCharTwoJEqZeroNF

Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

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

English

The invariant c4 is minus forty-eight times a4: c4 = -48 a4.

Русский

Инвариант c4 равен минус 48 раз a4: c4 = -48 a4.

LaTeX

$$$W.c_4 = -48 \; W.a_4$$$

Lean4

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

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

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

Разделы

Аффилиация

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